From c034197e869cdc418b225b9abf25dee63a47e237 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 5 Mar 2001 14:11:40 +0000
Subject: 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
---
 proofs/clenv.ml | 29 +++++++++++++++++------------
 1 file changed, 17 insertions(+), 12 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f7ec080301..31555eaa89 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"))
 
-- 
cgit v1.2.3