diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-05 16:48:30 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-05 16:48:30 +0000 |
commit | b91f60aab99980b604dc379b4ca62f152315c841 (patch) | |
tree | cd1948fc5156988dd74d94ef4abb3e4ac77e3de8 /pretyping/indrec.mli | |
parent | 2ff72589e5c90a25b315922b5ba2d7c11698adef (diff) |
GROS COMMIT:
- reduction du noyau (variables existentielles, fonctions auxiliaires
pour inventer des noms, etc. deplacees hors de kernel/)
- changement de noms de constructeurs des constr (suppression de "Is" et
"Mut")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |