Merge branch 'v8.5'

2 files changed, 29 insertions, 0 deletions

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.
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.           
+