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

8 files changed, 47 insertions, 33 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index d12c3a213..5237b93db 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -28,8 +28,8 @@ open Entries
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
+(* Errors related to inductive constructions *)
 type inductive_error =
-  (* These are errors related to inductive constructions in this module *)
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
   | NotConstructor of env * constr * constr
@@ -39,10 +39,6 @@ type inductive_error =
   | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
-  (* These are errors related to recursors building in Indrec *)
-  | NotAllowedCaseAnalysis of bool * sorts * inductive
-  | BadInduction of bool * identifier * sorts
-  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index bbfa47818..05534ec36 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -22,8 +22,8 @@ open Typeops
 (*s The different kinds of errors that may result of a malformed inductive
   definition. *)
 
+(* Errors related to inductive constructions *)
 type inductive_error =
-  (* These are errors related to inductive constructions in this module *)
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
   | NotConstructor of env * constr * constr
@@ -33,10 +33,6 @@ type inductive_error =
   | SameNamesOverlap of identifier list
   | NotAnArity of identifier
   | BadEntry
-  (* These are errors related to recursors building in Indrec *)
-  | NotAllowedCaseAnalysis of bool * sorts * inductive
-  | BadInduction of bool * identifier * sorts
-  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0325a3acd..b0dcdde0d 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -23,11 +23,18 @@ open Environ
 open Reductionops
 open Typeops
 open Type_errors
-open Indtypes (* pour les erreurs *)
 open Safe_typing
 open Nametab
 open Sign
 
+(* 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
+
 let make_prod_dep dep env = if dep then prod_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
@@ -442,7 +449,7 @@ let make_case_gen env   = make_case_com None env
 
 
 (**********************************************************************)
-(* [instanciate_indrec_scheme s rec] replace the sort of the scheme
+(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
    [rec] by [s] *)
 
 let change_sort_arity sort = 
@@ -456,7 +463,7 @@ let change_sort_arity sort =
   drec 
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
-let instanciate_indrec_scheme sort =
+let instantiate_indrec_scheme sort =
   let rec drec npar elim =
     match kind_of_term elim with
       | Lambda (n,t,c) -> 
@@ -465,13 +472,13 @@ let instanciate_indrec_scheme sort =
 	  else 
 	    mkLambda (n, t, drec (npar-1) c)
       | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "instanciate_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
   in
   drec
 
 (* Change the sort in the type of an inductive definition, builds the
    corresponding eta-expanded term *)
-let instanciate_type_indrec_scheme sort npars term =
+let instantiate_type_indrec_scheme sort npars term =
   let rec drec np elim =
     match kind_of_term elim with
       | Prod (n,t,c) -> 
@@ -484,7 +491,7 @@ let instanciate_type_indrec_scheme sort npars term =
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
            mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') 
-      | _ -> anomaly "instanciate_type_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
   in
   drec npars
 
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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 26848802e..ee9959a69 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -46,19 +46,16 @@ exception RefinerError of refiner_error
 
 open Pretype_errors
 
-let catchable_exception = function
-  | Util.UserError _ | TypeError _ | RefinerError _
+let rec catchable_exception = function
+  | Stdpp.Exc_located(_,e) -> catchable_exception e
+  | Util.UserError _ | TypeError _ 
+  | RefinerError _ | Indrec.RecursionSchemeError _
+  | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
   (* unification errors *)
   | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _|
-      CannotUnifyBindingType _|NotClean _))
-  | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _|
-          NoOccurrenceFound _ | CannotUnifyBindingType _|NotClean _)))
-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
-    Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
-    | Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ )))-> true
+      CannotUnifyBindingType _|NotClean _)) -> true
   | _ -> false
 
-
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
 let check = ref false
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 913f1250d..8a4487727 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -76,6 +76,8 @@ let rec explain_exn_default = function
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
   | InductiveError e -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
+  | RecursionSchemeError e -> 
+      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,e) -> 
       hov 0
 	(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 55201ea43..40fae1e8f 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -586,8 +586,9 @@ let error_bad_induction dep indid kind =
 let error_not_mutual_in_scheme () =
  str "Induction schemes are concerned only with distinct mutually inductive types"
 
+(* Inductive constructions errors *)
+
 let explain_inductive_error = function
-  (* These are errors related to inductive constructions *)
   | NonPos (env,c,v) -> error_non_strictly_positive env c v
   | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v
   | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v
@@ -597,7 +598,10 @@ let explain_inductive_error = function
   | SameNamesOverlap idl -> error_same_names_overlap idl
   | NotAnArity id -> error_not_an_arity id
   | BadEntry -> error_bad_entry ()
-  (* These are errors related to recursors *)
+
+(* Recursion schemes errors *)
+
+let explain_recursion_scheme_error = function
   | NotAllowedCaseAnalysis (dep,k,i) ->
       error_not_allowed_case_analysis dep k i
   | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 1c389b9c2..2625243dc 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -27,6 +27,8 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds
 
 val explain_inductive_error : inductive_error -> std_ppcmds
 
+val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
+
 val explain_refiner_error : refiner_error -> std_ppcmds
 
 val explain_pattern_matching_error :