3 files changed, 62 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7421.v b/test-suite/bugs/closed/7421.v
new file mode 100644
index 0000000000..afcdd35fcc
--- /dev/null
+++ b/test-suite/bugs/closed/7421.v
@@ -0,0 +1,39 @@
+
+
+Universe i j.
+
+Goal False.
+Proof.
+  Check Type@{i} : Type@{j}.
+  Fail constr_eq_strict Type@{i} Type@{j}.
+  assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
+  Fail constr_eq_strict Type@{i} Type@{j}.
+
+  constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
+  constr_eq_strict Type@{i} Type@{j}.
+  Fail Check Type@{i} : Type@{j}.
+
+  Fail constr_eq Prop Set.
+  Fail constr_eq Prop Type.
+
+  Fail constr_eq_strict Type Type.
+  constr_eq Type Type.
+
+  constr_eq_strict Set Set.
+  constr_eq Set Set.
+  constr_eq Prop Prop.
+
+  let x := constr:(Type) in constr_eq_strict x x.
+  let x := constr:(Type) in constr_eq x x.
+
+  Fail lazymatch type of prod with
+       | ?A -> ?B -> _ => constr_eq_strict A B
+       end.
+  lazymatch type of prod with
+  | ?A -> ?B -> _ => constr_eq A B
+  end.
+  lazymatch type of prod with
+  | ?A -> ?B -> ?C => constr_eq A C
+  end.
+
+Abort.
diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v
index de2857b437..2f0d8bf8c4 100644
--- a/test-suite/success/letproj.v
+++ b/test-suite/success/letproj.v
@@ -7,3 +7,5 @@ Definition test (A : Type) (f : Foo A) :=
 
 Scheme foo_case := Case for Foo Sort Type.
 
+Definition test' (A : Type) (f : Foo A) :=
+  let 'Build_Foo _ x y := f in x.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 31a1608c4d..7ca2767a53 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -199,3 +199,24 @@ split.
 reflexivity.
 Qed.
 *)
+
+(* 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 *)