From cc2e8c9e7f8d414ed34e6e39b4df18a76ade35b4 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 12 Feb 2002 10:56:10 +0000
Subject: petite modif pour ne pas expanser trop de let pendant l'unification

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

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 43a07aa1a5..be9bd638ac 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -175,6 +175,7 @@ let unify_0 cv_pb mc wc m n =
 	      error_cannot_unify (m,n)
 
 	| LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
+	| _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
 		
 	| _ -> error_cannot_unify (m,n)
 	      
-- 
cgit v1.2.3