I was wondering whether there is a way to let Coq generate dependent Case Analysis principles using the Scheme command.
I found the five kinds “Induction”, “Minimality”, “Elimination”, “Case” and “Equality” inside g_vernac.ml.
Where Elimination and Case should produce a case analysis principle (case non-dependent and elimination dependent).
As far as I see the generated principles coincide with “Minimality” and “Induction” as they are recursive and include inductive hypothesis for recursive instances of the inductive type.
Therefore my question is how the commands differ in practice and if there is a command for nonrecursive dependent case analysis principles.
It sounds like a bug that the two different names produce the same elimination principles 
IIRC the code is able to generate recursive and non-recursive versions of the eliminators.
1 Like