From e5fe4569f3eaeaa4e1ce377989e19f1f2c176da9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 Apr 2016 00:02:32 +0200
Subject: An example for cd139311e, showing a consequence of not converting
 constants up to their canonical name (taken from Daniel's formalization of
 Puiseux theorem).

---
 test-suite/success/remember.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054a3..b26a9ff1eb 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -14,3 +14,16 @@ let name := fresh "fresh" in
 remember (1 + 2) as x eqn:name.
 rewrite fresh.
 Abort.
+
+(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
+                  
+Module A.
+Axiom N : nat.
+End A.
+Module B.
+Include A.
+End B.
+Goal id A.N = B.N.
+reflexivity.
+Qed.           
+                
-- 
cgit v1.2.3


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')

diff --git a/test-suite/bugs/closed/4634.v b/test-suite/bugs/closed/4634.v
new file mode 100644
index 0000000000..77e31e108f
--- /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