Amélioration message d'erreur objet de récursion de type non inductif

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

4 files changed, 10 insertions, 8 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5b2e8998b..3e2f03871 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -668,8 +668,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     or bodynum >= nbfix
   then anomaly "Ill-formed fix term";
   let fixenv = push_rec_types recdef env in
-  let raise_err i err =
-    error_ill_formed_rec_body fixenv err names i in
+  let raise_err env i err =
+    error_ill_formed_rec_body env err names i in
   (* Check the i-th definition with recarg k *)
   let find_ind i k def = 
     if k < 0 then anomaly "negative recarg position";
@@ -684,11 +684,12 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) = 
                   try find_inductive env a 
-                  with Not_found -> raise_err i RecursionNotOnInductiveType in
+                  with Not_found ->
+		    raise_err env i (RecursionNotOnInductiveType a) in
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
             else anomaly "check_one_fix: Bad occurrence of recursive call"
-        | _ -> raise_err i NotEnoughAbstractionInFixBody in
+        | _ -> raise_err env i NotEnoughAbstractionInFixBody in
     check_occur fixenv 1 def in
   (* Do it on every fixpoint *)
   let rv = array_map2_i find_ind nvect bodies in
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 73aaaed93..9e8d58fa8 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -19,7 +19,7 @@ open Reduction
 type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType
+  | RecursionNotOnInductiveType of constr
   | RecursionOnIllegalTerm of int * constr * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index f9f2e04a4..ffa16968c 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -21,7 +21,7 @@ open Environ
 type guard_error =
   (* Fixpoints *)
   | NotEnoughAbstractionInFixBody
-  | RecursionNotOnInductiveType
+  | RecursionNotOnInductiveType of constr
   | RecursionOnIllegalTerm of int * constr * int list * int list
   | NotEnoughArgumentsForFixCall of int
   (* CoFixpoints *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 82aad5a6d..9d2160cb6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -222,8 +222,9 @@ let explain_ill_formed_rec_body ctx err names i =
   (* Fixpoint guard errors *)
   | NotEnoughAbstractionInFixBody ->
       str "Not enough abstractions in the definition"
-  | RecursionNotOnInductiveType ->
-      str "Recursive definition on a non inductive type"
+  | RecursionNotOnInductiveType c ->
+      str "Recursive definition on" ++ spc() ++ prterm_env ctx c ++ spc() ++
+      str "which should be an inductive type"
   | RecursionOnIllegalTerm(j,arg,le,lt) ->
       let called =
         match names.(j) with