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
---
 pretyping/evarutil.ml | 1 -
 proofs/clenv.ml       | 1 +
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 4ccf4817cd..a53ecf5355 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -71,7 +71,6 @@ let whd_castappevar_stack sigma c =
 	  whrec (existential_value sigma (ev,args), l)
       | Cast (c,_) -> whrec (c, l)
       | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
-      | LetIn (_,v,_,b) -> whrec (subst1 v b, l)
       | _ -> s
   in 
   whrec (c, [])
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