From 016f2dc3aee608b149097cc08d0720227addc18a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 29 Apr 2016 11:13:54 +0200 Subject: 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. --- test-suite/bugs/closed/4634.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 test-suite/bugs/closed/4634.v (limited to 'test-suite/bugs/closed/4634.v') 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. -- cgit v1.2.3