Module Induction

Elimination tactics.
type elim_scheme = {
elimt : EConstr.types;
indref : Names.GlobRef.t option;
params : EConstr.rel_context;(*

(prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)

*)
nparams : int;(*

number of parameters

*)
predicates : EConstr.rel_context;(*

(Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)

*)
npredicates : int;(*

Number of predicates

*)
branches : EConstr.rel_context;(*

branchr,...,branch1

*)
nbranches : int;(*

Number of branches

*)
args : EConstr.rel_context;(*

(xni, Ti_ni) ... (x1, Ti_1)

*)
nargs : int;(*

number of arguments

*)
indarg : EConstr.rel_declaration option;(*

Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise

*)
concl : EConstr.types;(*

Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive

*)
indarg_in_concl : bool;(*

true if HI appears at the end of conclusion

*)
farg_in_concl : bool;(*

true if (f...) appears at the end of conclusion

*)
}

rel_contexts and rel_declaration actually contain triples, and lists are actually in reverse order to fit compose_prod.

val compute_elim_sig : Evd.evar_map -> EConstr.types -> elim_scheme
Generic case analysis / induction tactics.

Implements user-level "destruct" and "induction"