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 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping')

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, [])
-- 
cgit v1.2.3