Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 29 insertions, 1 deletions

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 31a1608c..299b08bd 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -193,9 +193,37 @@ 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.
+Set Primitive Projections.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments pair {_ _} _ _.
+
+Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) :=
+  match n with
+  | 0 => pair nil l
+  | S n =>
+    match l with
+    | nil => pair nil nil
+    | x :: l => let 'pair l1 l2 := split_at l n in pair (x :: l1) l2
+    end
+  end.
+
+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)).