From 2e42df1fe1e4b8276e7a4b268002e6a68d3ac619 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Aug 2004 18:15:24 +0000
Subject: 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
---
 kernel/inductive.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5b2e8998bf..3e2f03871a 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
-- 
cgit v1.2.3