From 978ae7d9323558099efb0c4e4e39549221378d5d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Oct 2014 16:55:56 +0200
Subject: To stay closer to non-primitive projections, only unfold primitive
 projections in cbv when delta _and_ beta flags are set. Add test-suite file
 for bug 3700 too.

---
 pretyping/cbv.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 4db9cf0661..0e7804bc7d 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -200,8 +200,9 @@ let rec norm_head info env t stack =
   
   | Proj (p, c) -> 
     let p' =
-      if red_set (info_flags info) (fCONST (Projection.constant p)) then
-	Projection.unfold p
+      if red_set (info_flags info) (fCONST (Projection.constant p)) 
+      	&& red_set (info_flags info) fBETA 
+      then Projection.unfold p
       else p
     in 
     let pinfo = Environ.lookup_projection p (info_env info) in
-- 
cgit v1.2.3