From fd07bda1ac92972c4224868f6d9dfeb430b7f379 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Jan 2001 15:25:14 +0000
Subject: Retour en arrière sur le pb f_equal en attente meilleure solution

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1265 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index da4233c721..2093311851 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -579,7 +579,7 @@ let clenv_merge with_types =
     	  else
 	    let mc,ec =
 	      let mvty = clenv_instance_type clenv mv in
-	      if with_types or occur_meta mvty then
+	      if with_types (* or occur_meta mvty *) then
 		let nty = clenv_type_of clenv 
 			    (clenv_instance clenv (mk_freelisted n)) in
 		unify_0 [] clenv.hook mvty nty
-- 
cgit v1.2.3