Module InductionSource

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

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

    *)
  4. nparams : int;
    (*

    number of parameters

    *)
  5. predicates : EConstr.rel_context;
    (*

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

    *)
  6. npredicates : int;
    (*

    Number of predicates

    *)
  7. branches : EConstr.rel_context;
    (*

    branchr,...,branch1

    *)
  8. nbranches : int;
    (*

    Number of branches

    *)
  9. args : EConstr.rel_context;
    (*

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

    *)
  10. nargs : int;
    (*

    number of arguments

    *)
  11. indarg : EConstr.rel_declaration option;
    (*

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

    *)
  12. concl : EConstr.types;
    (*

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

    *)
  13. indarg_in_concl : bool;
    (*

    true if HI appears at the end of conclusion

    *)
  14. 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.

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

Implements user-level "destruct" and "induction"