1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
new file mode 100644
index 000000000..2682df3b7
--- /dev/null
+++ b/test-suite/success/primitiveproj.v
@@ -0,0 +1,30 @@
+Set Primitive Projections.
+Set Record Elimination Schemes.
+Module Prim.
+
+Record F := { a : nat; b : a = a }.
+Record G (A : Type) := { c : A; d : F }.
+
+Check c.
+End Prim.
+Module Univ.
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Record Foo (A : Type) := { foo : A }.
+
+Record G (A : Type) := { c : A; d : c = c; e : Foo A }.
+
+Definition Foon : Foo nat := {| foo := 0 |}.
+
+Definition Foonp : nat := Foon.(foo).
+
+Definition Gt : G nat := {| c:= 0; d:=eq_refl; e:= Foon |}.
+
+Check (Gt.(e)).
+
+Section bla.
+
+  Record bar := { baz : nat; def := 0; baz' : forall x, x = baz \/ x = def }.
+End bla.
+
+End Univ.