module Explore générique et réécriture EAuto avec ce module; occur check dans clenv_merge

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

1 files changed, 17 insertions, 12 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f7ec08030..31555eaa8 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -556,18 +556,23 @@ let clenv_merge with_types =
     	      if w_defined_evar clenv.hook evn then
 		let (metas',evars') = unify_0 [] clenv.hook rhs lhs in
 		clenv_resrec (metas'@metas) (evars'@t) clenv
-    	      else
-		(try let rhs' = if occur_meta rhs then subst_meta metas rhs else rhs in
-		   clenv_resrec metas t
-		     (clenv_wtactic (w_Define evn rhs') clenv)
-		 with ex when catchable_exception ex ->
-		   (match krhs with
-		      | IsApp (f,cl) when isConst f or isMutConstruct f ->
-			  clenv_resrec metas evars 
-			    (clenv_wtactic
-			       (mimick_evar f (Array.length cl) evn)
-			       clenv)
-           	      | _ -> error "w_Unify"))
+    	      else begin
+		let rhs' = 
+		  if occur_meta rhs then subst_meta metas rhs else rhs 
+		in
+		if occur_evar evn rhs' then error "w_Unify";
+		try 
+		  clenv_resrec metas t 
+		    (clenv_wtactic (w_Define evn rhs') clenv)
+		with ex when catchable_exception ex ->
+		  (match krhs with
+		     | IsApp (f,cl) when isConst f or isMutConstruct f ->
+			 clenv_resrec metas evars 
+			   (clenv_wtactic
+			      (mimick_evar f (Array.length cl) evn)
+			      clenv)
+           	     | _ -> error "w_Unify")
+	      end
 
 	  | _ -> anomaly "clenv_resrec"))