diff options
Diffstat (limited to 'pretyping/indrec.mli')
-rw-r--r-- | pretyping/indrec.mli | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli new file mode 100644 index 000000000..7e6dd8fa1 --- /dev/null +++ b/pretyping/indrec.mli @@ -0,0 +1,54 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Names +open Term +open Declarations +open Inductiveops +open Environ +open Evd +(*i*) + +(* Eliminations. *) + +(* These functions build elimination predicate for Case tactic *) + +val make_case_dep : env -> 'a evar_map -> inductive -> sorts_family -> constr +val make_case_nodep : env -> 'a evar_map -> inductive -> sorts_family -> constr +val make_case_gen : env -> 'a evar_map -> inductive -> sorts_family -> constr + +(* This builds an elimination scheme associated (using the own arity + of the inductive) *) + +val build_indrec : env -> 'a evar_map -> inductive -> constr +val instanciate_indrec_scheme : sorts -> int -> constr -> constr + +(* This builds complex [Scheme] *) + +val build_mutual_indrec : + env -> 'a evar_map -> + (inductive * mutual_inductive_body * one_inductive_body + * bool * sorts_family) list + -> constr list + +(* These are for old Case/Match typing *) + +val type_rec_branches : bool -> env -> 'c evar_map -> inductive_type + -> unsafe_judgment -> constr -> constr array * constr +val make_rec_branch_arg : + env -> 'a evar_map -> + int * ('b * constr) option array * int -> + constr -> constructor_summary -> recarg list -> constr + +(* *) +val declare_eliminations : mutual_inductive -> unit +val lookup_eliminator : inductive -> sorts_family -> constr +val elimination_suffix : sorts_family -> string |