From ae6c95a3755fc3a9434bcc9fdd81b7c69baa8280 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 17 Dec 2005 21:13:48 +0000
Subject: Création d'un type d'erreur RecursionSchemeError distinct de
 InductiveError et suite correction bug #1028
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/indrec.mli | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'pretyping/indrec.mli')

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
-- 
cgit v1.2.3