From d2a3ef20b7605a5e3b12b37d2519322e4a7085bf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 12 Mar 2001 14:28:59 +0000
Subject: Amélioration message d'erreur conditions de garde

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1455 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7b6e58c83c..694d9ae778 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -712,12 +712,12 @@ let check_fix env sigma ((nvect,bodynum),(types,names,bodies as recdef)) =
     or bodynum >= nbfix
   then anomaly "Ill-formed fix term";
   for i = 0 to nbfix - 1 do
+    let fixenv = push_rec_types recdef env in
     try
-      let fixenv = push_rec_types recdef env in
       let _ = check_subterm_rec_meta fixenv sigma nvect nvect.(i) bodies.(i)
       in ()
     with FixGuardError err ->
-      error_ill_formed_rec_body	CCI env err (List.rev names) i bodies
+      error_ill_formed_rec_body	CCI fixenv err (List.rev names) i bodies
   done 
 
 (*
@@ -850,12 +850,12 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 let check_cofix env sigma (bodynum,(types,names,bodies as recdef)) = 
   let nbfix = Array.length bodies in 
   for i = 0 to nbfix-1 do
+    let fixenv = push_rec_types recdef env in
     try 
-      let fixenv = push_rec_types recdef env in
       let _ = check_guard_rec_meta fixenv sigma nbfix bodies.(i) types.(i)
       in ()
     with CoFixGuardError err -> 
-      error_ill_formed_rec_body CCI env err (List.rev names) i bodies
+      error_ill_formed_rec_body CCI fixenv err (List.rev names) i bodies
   done
 
 (* Checks the type of a (co)fixpoint.
-- 
cgit v1.2.3