Fix incorrect cbv reduction of primitive projections. (Bug #4634)

As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.

The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4634.v b/test-suite/bugs/closed/4634.v
new file mode 100644
index 000000000..77e31e108
--- /dev/null
+++ b/test-suite/bugs/closed/4634.v
@@ -0,0 +1,16 @@
+Set Primitive Projections.
+
+Polymorphic Record pair {A B : Type} : Type :=
+  prod { pr1 : A; pr2 : B }.
+
+Notation " ( x ; y ) " := (@prod _ _ x y).
+Notation " x .1 " := (pr1 x) (at level 3).
+Notation " x .2 " := (pr2 x) (at level 3).
+
+Goal ((0; 1); 2).1.2 = 1.
+Proof.
+  cbv.
+  match goal with
+  | |- ?t = ?t => exact (eq_refl t)
+  end.
+Qed.