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 00000000..77e31e10
--- /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.