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.

2 files changed, 87 insertions, 2 deletions

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
diff --git a/test-suite/bugs/closed/3700.v b/test-suite/bugs/closed/3700.v
new file mode 100644
index 0000000000..4e226524cb
--- /dev/null
+++ b/test-suite/bugs/closed/3700.v
@@ -0,0 +1,84 @@
+
+Set Implicit Arguments.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record prod A B := pair { fst : A ; snd : B }.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record prod A B := pair { fst : A ; snd : B }.
+End Prim.
+Goal (forall x : NonPrim.prod Set Set, let (a, b) := x in a = a)
+/\ (forall x : Prim.prod Set Set, let (a, b) := x in a = a).
+  Show. (* (forall x : NonPrim.prod Set Set, let (a, _) := x in a = a) /\
+   (forall x : Prim.prod Set Set,
+    let a := Prim.fst x in let b := Prim.snd x in a = a) *)
+  Set Printing All.
+  Show. (* and
+     (forall x : NonPrim.prod Set Set,
+      match x return Prop with
+      | NonPrim.pair a _ => @eq Set a a
+      end)
+     (forall x : Prim.prod Set Set,
+      let a := @Prim.fst Set Set x in
+      let b := @Prim.snd Set Set x in @eq Set a a) *)
+  Unset Printing All.
+Abort.
+Goal (forall x : NonPrim.prod Set Set, match x with NonPrim.pair a b => a = a end)
+/\ (forall x : Prim.prod Set Set, match x with Prim.pair a b => a = a end).
+  Show. (* (forall x : NonPrim.prod Set Set,
+    match x with
+    | {| NonPrim.fst := a |} => a = a
+    end) /\ (forall x : Prim.prod Set Set, Prim.fst x = Prim.fst x) *)
+  (** Wrong: [match] should generate unfolded things *)
+  Set Printing All.
+  Show. (* and
+     (forall x : NonPrim.prod Set Set,
+      match x return Prop with
+      | NonPrim.pair a _ => @eq Set a a
+      end)
+     (forall x : Prim.prod Set Set,
+      @eq Set (@Prim.fst Set Set x) (@Prim.fst Set Set x)) *)
+  Unset Printing All.
+Abort.
+Goal (forall x : NonPrim.prod Set Set, let (a, b) := x in a = a /\ b = b)
+/\ (forall x : Prim.prod Set Set, let (a, b) := x in a = a /\ b = b).
+  Show. (* (forall x : NonPrim.prod Set Set, let (a, b) := x in a = a /\ b = b) /\
+   (forall x : Prim.prod Set Set,
+    let a := Prim.fst x in let b := Prim.snd x in a = a /\ b = b) *)
+  (** Understandably different, maybe, but should still be unfolded *)
+  Set Printing All.
+  Show. (* and
+     (forall x : NonPrim.prod Set Set,
+      match x return Prop with
+      | NonPrim.pair a b => and (@eq Set a a) (@eq Set b b)
+      end)
+     (forall x : Prim.prod Set Set,
+      let a := @Prim.fst Set Set x in
+      let b := @Prim.snd Set Set x in and (@eq Set a a) (@eq Set b b)) *)
+  Unset Printing All.
+Abort.
+Goal (forall x : NonPrim.prod Set Set, match x with NonPrim.pair a b => a = a /\ b = b end)
+/\ (forall x : Prim.prod Set Set, match x with Prim.pair a b => a = a /\ b = b end).
+  Show. (* (forall x : NonPrim.prod Set Set,
+    match x with
+    | {| NonPrim.fst := a; NonPrim.snd := b |} => a = a /\ b = b
+    end) /\
+   (forall x : Prim.prod Set Set,
+    Prim.fst x = Prim.fst x /\ Prim.snd x = Prim.snd x) *)
+  Set Printing All.
+  Show.
+
+  set(foo:=forall x : Prim.prod Set Set, match x return Set with
+                 | Prim.pair fst _ => fst
+                 end).
+  (* and
+     (forall x : NonPrim.prod Set Set,
+      match x return Prop with
+      | NonPrim.pair a b => and (@eq Set a a) (@eq Set b b)
+      end)
+     (forall x : Prim.prod Set Set,
+      and (@eq Set (@Prim.fst Set Set x) (@Prim.fst Set Set x))
+        (@eq Set (@Prim.snd Set Set x) (@Prim.snd Set Set x))) *)
+  Unset Printing All.
+Abort.
\ No newline at end of file