diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-17 21:13:48 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-17 21:13:48 +0000 |
commit | ae6c95a3755fc3a9434bcc9fdd81b7c69baa8280 (patch) | |
tree | 695244819d00b4816223e572c7867ca21efa9758 /pretyping/indrec.mli | |
parent | cea2061080d540c0507192eca1887ea4b502680d (diff) |
Création d'un type d'erreur RecursionSchemeError distinct de InductiveError et suite correction bug #1028
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/indrec.mli')
-rw-r--r-- | pretyping/indrec.mli | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 2306201b2..f0f7747cb 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -17,7 +17,16 @@ open Environ open Evd (*i*) -(* Eliminations. *) +(* Errors related to recursors building *) + +type recursion_scheme_error = + | NotAllowedCaseAnalysis of bool * sorts * inductive + | BadInduction of bool * identifier * sorts + | NotMutualInScheme + +exception RecursionSchemeError of recursion_scheme_error + +(** Eliminations *) (* These functions build elimination predicate for Case tactic *) @@ -29,11 +38,11 @@ val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr of the inductive) *) val build_indrec : env -> evar_map -> inductive -> constr -val instanciate_indrec_scheme : sorts -> int -> constr -> constr -val instanciate_type_indrec_scheme : sorts -> int -> constr -> types -> +val instantiate_indrec_scheme : sorts -> int -> constr -> constr +val instantiate_type_indrec_scheme : sorts -> int -> constr -> types -> constr * types -(* This builds complex [Scheme] *) +(** Complex recursion schemes [Scheme] *) val build_mutual_indrec : env -> evar_map -> @@ -41,7 +50,7 @@ val build_mutual_indrec : * bool * sorts_family) list -> constr list -(* These are for old Case/Match typing *) +(** Old Case/Match typing *) val type_rec_branches : bool -> env -> evar_map -> inductive_type -> constr -> constr -> constr array * constr @@ -50,7 +59,8 @@ val make_rec_branch_arg : int * ('b * constr) option array * int -> constr -> constructor_summary -> wf_paths list -> constr -(* *) +(** Recursor names utilities *) + val lookup_eliminator : inductive -> sorts_family -> constr val elimination_suffix : sorts_family -> string val make_elimination_ident : identifier -> sorts_family -> identifier |