- amelioration des messages d'erreur de la condition de garde

- restructuration de clenv.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3455 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index a18ffd7e5..b194dac97 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -22,8 +22,8 @@ type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
   | RecursionNotOnInductiveType
-  | RecursionOnIllegalTerm
-  | NotEnoughArgumentsForFixCall
+  | RecursionOnIllegalTerm of int * constr * int list * int list
+  | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
   | CodomainNotInductiveType of constr
   | NestedRecursiveOccurrences
@@ -58,7 +58,7 @@ type type_error =
   | CantApplyBadType of
       (int * constr * constr) * unsafe_judgment * unsafe_judgment array
   | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
-  | IllFormedRecBody of guard_error * name array * int * constr array
+  | IllFormedRecBody of guard_error * name array * int
   | IllTypedRecBody of
       int * name array * unsafe_judgment array * types array
 
@@ -96,7 +96,7 @@ val error_cant_apply_bad_type :
       unsafe_judgment -> unsafe_judgment array -> 'a
 
 val error_ill_formed_rec_body :
-  env -> guard_error -> name array -> int -> constr array -> 'a
+  env -> guard_error -> name array -> int -> 'a
 
 val error_ill_typed_rec_body  :
   env -> int -> name array -> unsafe_judgment array -> types array -> 'a