diff options
Diffstat (limited to 'library/indrec.mli')
| -rw-r--r-- | library/indrec.mli | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/library/indrec.mli b/library/indrec.mli deleted file mode 100644 index aa3a0b6f1..000000000 --- a/library/indrec.mli +++ /dev/null @@ -1,47 +0,0 @@ -(***********************************************************************) -(* 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 Inductive -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_instance -> constr -val instanciate_indrec_scheme : sorts -> int -> constr -> constr - -(* This builds complex [Scheme] *) - -val build_mutual_indrec : - env -> 'a evar_map -> (inductive * 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 |