Fix #7329: coqchk Include with primitive projections

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/coqchk/include_primproj.v b/test-suite/coqchk/include_primproj.v
new file mode 100644
index 0000000000..804ba1d378
--- /dev/null
+++ b/test-suite/coqchk/include_primproj.v
@@ -0,0 +1,13 @@
+(* #7329 *)
+Set Primitive Projections.
+
+Module M.
+  Module Bar.
+    Record Box := box { unbox : Type }.
+
+    Axiom foo : Box.
+    Axiom baz : forall _ : unbox foo, unbox foo.
+  End Bar.
+End M.
+
+Include M.