4 files changed, 68 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_14131.v b/test-suite/bugs/closed/bug_14131.v
new file mode 100644
index 0000000000..611464458e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14131.v
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Unset Elimination Schemes.
+
+Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
+    JMeq_refl : JMeq x x.
+
+Set Elimination Schemes.
+
+Register JMeq as core.JMeq.type.
+
+Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
+  P x -> forall y, JMeq x y -> P y.
+
+Register JMeq_ind as core.JMeq.ind.
+
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
+   P x -> forall y, JMeq y x -> P y.
+Proof. intros. try rewrite H0.
+Abort.
diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v
new file mode 100644
index 0000000000..39b620a6ac
--- /dev/null
+++ b/test-suite/ltac2/std_tactics.v
@@ -0,0 +1,29 @@
+Require Import Ltac2.Ltac2.
+
+Axiom f: nat -> nat.
+Definition g := f.
+
+Axiom Foo1: nat -> Prop.
+Axiom Foo2: nat -> Prop.
+Axiom Impl: forall n: nat, Foo1 (f n) -> Foo2 (f n).
+
+Create HintDb foo discriminated.
+#[export] Hint Constants Opaque : foo.
+#[export] Hint Resolve Impl : foo.
+
+Goal forall x, Foo1 (f x) -> Foo2 (g x).
+Proof.
+  auto with foo.
+  #[export] Hint Transparent g : foo.
+  auto with foo.
+Qed.
+
+Goal forall (x: nat), exists y, f x = g y.
+Proof.
+  intros.
+  eexists.
+  unify f g.
+  lazy_match! goal with
+  | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs
+  end.
+Abort.
diff --git a/test-suite/micromega/bug_11089.v b/test-suite/micromega/bug_11089.v
new file mode 100644
index 0000000000..e62b5b8d9e
--- /dev/null
+++ b/test-suite/micromega/bug_11089.v
@@ -0,0 +1,13 @@
+Require Import Lia.
+Unset Lia Cache.
+Definition t := nat.
+Goal forall (n : t), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
+Goal let t' := nat in forall (n : t'), n = n.
+Proof.
+  intros.
+  lia.
+Qed.
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index a12623c3c0..2ea320047d 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -167,6 +167,12 @@ Goal  @zero znat = 0%nat.
   reflexivity.
 Qed.
 
+Require Import ZifyBool.
+Instance Op_bool_inj : UnOp (inj : bool -> bool) :=
+  { TUOp := id; TUOpInj := fun _ => eq_refl }.
+Add Zify UnOp Op_bool_inj.
+
+
 Goal forall (x y : positive) (F : forall (P: Pos.le x y) , positive) (P : Pos.le x y),
     (F P + 1 = 1 + F P)%positive.
 Proof.
@@ -228,6 +234,7 @@ Proof.
   intros. lia.
 Qed.
 
+
 Ltac Zify.zify_pre_hook ::= unfold is_true in *.
 
 Goal forall x y : nat, is_true (Nat.eqb x 1) ->