summaryrefslogtreecommitdiff
path: root/pretyping/indrec.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /pretyping/indrec.mli
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'pretyping/indrec.mli')
-rw-r--r--pretyping/indrec.mli27
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
+
+
+