5 files changed, 94 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/bug_10757.v b/test-suite/bugs/closed/bug_10757.v
new file mode 100644
index 0000000000..a531f6e563
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10757.v
@@ -0,0 +1,38 @@
+Require Import Program Extraction ExtrOcamlBasic.
+Print sig.
+Section FIXPOINT.
+
+Variable A: Type.
+
+Variable eq: A -> A -> Prop.
+Variable beq: A -> A -> bool.
+Hypothesis beq_eq: forall x y, beq x y = true -> eq x y.
+Hypothesis beq_neq: forall x y, beq x y = false -> ~eq x y.
+
+Variable le: A -> A -> Prop.
+Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
+
+Definition gt (x y: A) := le y x /\ ~eq y x.
+Hypothesis gt_wf: well_founded gt.
+
+Variable F: A -> A.
+Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).
+
+Program Fixpoint iterate
+    (x: A) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z)
+    {wf gt x}
+    : {y : A | eq y (F y) /\ forall z, le (F z) z -> le y z } :=
+  let x' := F x in
+  match beq x x' with
+  | true  => x
+  | false => iterate x' _ _
+  end.
+Next Obligation.
+  split.
+- auto.
+- apply beq_neq. auto.
+Qed.
+
+End FIXPOINT.
+
+Recursive Extraction iterate.
diff --git a/test-suite/bugs/closed/bug_10778.v b/test-suite/bugs/closed/bug_10778.v
new file mode 100644
index 0000000000..25d729b7e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10778.v
@@ -0,0 +1,32 @@
+(* Test that fresh avoid the variables of intro patterns but also of
+   simple intro patterns *)
+
+Ltac exploit_main t T pat cleanup
+  :=
+  (lazymatch T with
+   | ?U1 -> ?U2 =>
+       let H := fresh
+       in
+idtac "H=" H;
+         assert U1 as H;
+         [cleanup () | exploit_main (t H) U2 pat ltac:(fun _ => clear H; cleanup ())]
+   | _ =>
+       pose proof t as pat;
+       cleanup ()
+   end).
+
+Tactic Notation "exploit" constr(t) "as" simple_intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit H0 as H.
+Abort.
+
+Tactic Notation "exploit'" constr(t) "as" intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit' H0 as H.
+Abort.
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
new file mode 100644
index 0000000000..39601d99a8
--- /dev/null
+++ b/test-suite/ltac2/constr.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
+Import Unsafe.
+
+Ltac2 Eval match (kind '(nat -> bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
+
+Set Allow StrictProp.
+Axiom something : SProp.
+Ltac2 Eval match (kind '(forall x : something, bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
diff --git a/test-suite/micromega/bug_9162.v b/test-suite/micromega/bug_9162.v
new file mode 100644
index 0000000000..4aedf57faf
--- /dev/null
+++ b/test-suite/micromega/bug_9162.v
@@ -0,0 +1,8 @@
+Require Import ZArith Lia.
+Local Open Scope Z_scope.
+
+Goal Z.of_N (Z.to_N 0) = 0.
+Proof. lia. Qed.
+
+Goal forall q, (Z.of_N (Z.to_N 0) = 0 -> q = 0) -> Z.of_N (Z.to_N 0) = q.
+Proof. lia. Qed.
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index 74f94a9bed..d293dc0533 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -196,7 +196,7 @@ Definition clone_subType U v :=
 
 Variable sT : subType.
 
-CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
+Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
 
 Lemma SubP u : Sub_spec u.
 Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed.
@@ -209,7 +209,7 @@ Definition insub x :=
 
 Definition insubd u0 x := odflt u0 (insub x).
 
-CoInductive insub_spec x : option sT -> Type :=
+Variant insub_spec x : option sT -> Type :=
   | InsubSome u of P x & val u = x : insub_spec x (Some u)
   | InsubNone   of ~~ P x          : insub_spec x None.
 
@@ -568,7 +568,7 @@ Fixpoint nth s n {struct n} :=
 
 Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z].
 
-CoInductive last_spec : seq T -> Type :=
+Variant last_spec : seq T -> Type :=
   | LastNil        : last_spec [::]
   | LastRcons s x  : last_spec (rcons s x).
 
@@ -1292,7 +1292,7 @@ Open Scope big_scope.
 (* packages both in in a term in which i occurs; it also depends on the       *)
 (* iterated <op>, as this can give more information on the expected type of   *)
 (* the <general_term>, thus allowing for the insertion of coercions.          *)
-CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
+Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
 
 Definition applybig {R I} (body : bigbody R I) x :=
   let: BigBody _ op b v := body in if b then op v x else x.