From a60e2ea37b953dbe76b2cf92e7fa06fcc5cc0c35 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 13 Jul 2004 14:16:53 +0000
Subject: bug #790: better error_not_clean

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

(limited to 'pretyping/evarutil.ml')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1ccf8f5230..9b29f47a65 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -283,7 +283,7 @@ let non_instantiated sigma =
  * false. The problem is that we won't get the right error message.
  *)
 
-let real_clean isevars ev args rhs =
+let real_clean env isevars ev args rhs =
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
@@ -309,7 +309,7 @@ let real_clean isevars ev args rhs =
   in
   let body = subs 0 rhs in
   if not (closed0 body)
-  then error_not_clean empty_env isevars.evars ev body;
+  then error_not_clean env isevars.evars ev body (evar_source ev isevars);
   body
 
 let make_evar_instance_with_rel env =
@@ -377,14 +377,14 @@ let new_isevar isevars env src typ =
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
 
-let evar_define isevars (ev,argsv) rhs =
+let evar_define env isevars (ev,argsv) rhs =
   if occur_evar ev rhs
-  then error_occur_check empty_env (evars_of isevars) ev rhs;
+  then error_occur_check env (evars_of isevars) ev rhs;
   let args = Array.to_list argsv in 
   let evd = ise_map isevars ev in
   (* the bindings to invert *)
   let worklist = make_subst (evar_env evd) args in
-  let body = real_clean isevars ev worklist rhs in
+  let body = real_clean env isevars ev worklist rhs in
   ise_define isevars ev body;
   [ev]
 
@@ -515,11 +515,11 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  solve_refl conv_algo env isevars n1 args1 args2
 	else
 	  if Array.length args1 < Array.length args2 then 
-	    evar_define isevars ev2 (mkEvar ev1)
+	    evar_define env isevars ev2 (mkEvar ev1)
 	  else 
-	    evar_define isevars ev1 t2
+	    evar_define env isevars ev1 t2
     | _ ->
-	evar_define isevars ev1 t2 in
+	evar_define env isevars ev1 t2 in
   let pbs = get_changed_pb isevars lsp in
   List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs
 
-- 
cgit v1.2.3