diff options
Diffstat (limited to 'pretyping/indrec.mli')
| -rw-r--r-- | pretyping/indrec.mli | 27 |
1 files changed, 20 insertions, 7 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index f6f76706..e5eb07f5 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indrec.mli,v 1.6.2.1 2004/07/16 19:30:45 herbelin Exp $ i*) +(*i $Id: indrec.mli 7660 2005-12-17 21:13:48Z herbelin $ i*) (*i*) open Names @@ -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,11 @@ 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 + + + |