From 9935f0d7ab63d31f7a4a8c05d90627dff41dabf8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 1 Mar 2002 16:51:20 +0000
Subject: Nouveau comportement: Delta ne s'applique pas aux variables liées par
 un let

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2506 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cbv.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index fa1d9fa3ad..d1d9206fab 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -207,7 +207,11 @@ let rec norm_head info env t stack =
       (* allow substitution but leave let's in place *)
       let zeta = red_set (info_flags info) fZETA in
       let env' =
-	if zeta or red_set (info_flags info) fDELTA then 
+	if zeta 
+          (* New rule: for Cbv, Delta does not apply to locally bound variables
+          or red_set (info_flags info) fDELTA
+          *)
+        then 
 	  subs_cons (cbv_stack_term info TOP env b,env)
 	else
 	  subs_lift env in
-- 
cgit v1.2.3