From a30be8ca7d6b7c6f17aa65de824e02194a7f3a9b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 22 Apr 2018 17:26:03 +0200
Subject: Fix #7329: coqchk Include with primitive projections

---
 test-suite/coqchk/include_primproj.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/coqchk/include_primproj.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From 277563ab74a0529c330343479a063f808baa6db4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 10 Jul 2018 15:34:22 +0200
Subject: Add simple test cases for vm and native on primitive projections.

---
 test-suite/success/primitiveproj.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 7ca2767a53..299b08bdd1 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -193,12 +193,13 @@ Set Primitive Projections.
 Record s (x:nat) (y:=S x) := {c:=x; d:x=c}.
 Lemma f : 0=1.
 Proof.
-Fail apply d.
+  Fail apply d.
 (*
 split.
 reflexivity.
 Qed.
 *)
+Abort.
 
 (* Primitive projection match compilation *)
 Require Import List.
@@ -220,3 +221,9 @@ Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) :=
 Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *)
 Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *)
 Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *)
+
+Check (@eq_refl _ 0 <: 0 = fst (pair 0 1)).
+Fail Check (@eq_refl _ 0 <: 0 = snd (pair 0 1)).
+
+Check (@eq_refl _ 0 <<: 0 = fst (pair 0 1)).
+Fail Check (@eq_refl _ 0 <<: 0 = snd (pair 0 1)).
-- 
cgit v1.2.3