8 files changed, 113 insertions, 7 deletions
diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/closed/bug_3166.v
index baf87631f0..3b3375fdd8 100644
--- a/test-suite/bugs/opened/bug_3166.v
+++ b/test-suite/bugs/closed/bug_3166.v
@@ -80,5 +80,5 @@ Goal forall T (x y : T) (p : x = y), True.
         ) as H0.
   compute in H0.
   change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
-  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
+  pose proof (fun k => @eq_trans _ _ _ k H0).
 Abort.
diff --git a/test-suite/bugs/closed/bug_6157.v b/test-suite/bugs/closed/bug_6157.v
new file mode 100644
index 0000000000..cd24e4c7ee
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6157.v
@@ -0,0 +1,15 @@
+(* Check that universe instances of refs are preserved *)
+
+Section U.
+Set Universe Polymorphism.
+Definition U@{i} := Type@{i}.
+
+Section foo.
+Universe i.
+Fail Check U@{i} : U@{i}.
+Notation Ui := U@{i}. (* syndef path *)
+Fail Check Ui : Type@{i}.
+Notation "#" := U@{i}. (* non-syndef path *)
+Fail Check # : Type@{i}.
+End foo.
+End U.
diff --git a/test-suite/micromega/reify_bool.v b/test-suite/micromega/reify_bool.v
new file mode 100644
index 0000000000..501fafc0b3
--- /dev/null
+++ b/test-suite/micromega/reify_bool.v
@@ -0,0 +1,18 @@
+Require Import ZArith.
+Require Import Lia.
+Import Z.
+Unset Lia Cache.
+
+Goal forall (x y : Z),
+   implb (Z.eqb x y) (Z.eqb y x) = true.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Goal forall (x y :Z), implb (Z.eqb x 0) (Z.eqb y 0) = true <->
+                      orb (negb (Z.eqb x 0))(Z.eqb y 0) = true.
+Proof.
+  intro.
+  lia.
+Qed.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 984ac4e527..6fd4d37ab4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -50,10 +50,11 @@ f =
 fun H : B =>
 match H with
 | AC x =>
-    let b0 := b in
-    (if b0 as b return (P b -> True)
-     then fun _ : P true => Logic.I
-     else fun _ : P false => Logic.I) x
+    (fun x0 : P b =>
+     let b0 := b in
+     (if b0 as b return (P b -> True)
+      then fun _ : P true => Logic.I
+      else fun _ : P false => Logic.I) x0) x
 end
      : B -> True
 The command has indeed failed with message:
diff --git a/test-suite/success/case_let_conversion.v b/test-suite/success/case_let_conversion.v
new file mode 100644
index 0000000000..3f1ab96fe1
--- /dev/null
+++ b/test-suite/success/case_let_conversion.v
@@ -0,0 +1,39 @@
+Axiom checker_flags : Set.
+
+Inductive Box (R : Type) : Type := box : Box R.
+
+Inductive typing (H : checker_flags) : Type :=
+| type_Rel : typing H -> typing H
+| type_Case : let i := tt in Box (typing H) -> typing H.
+
+Definition unbox (P : Type) (b : Box P) := match b with box _ => 0 end.
+
+Definition size (H : checker_flags) (d : typing H) : nat.
+Proof.
+revert d.
+fix size 1.
+destruct 1.
+- exact (size d).
+- exact (unbox _ b).
+Defined.
+
+Definition foo (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+simpl.
+reflexivity.
+Qed.
+
+Definition bar (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Definition qux (H : checker_flags) (a : typing H) :
+  size H (type_Rel H a) = size H a.
+Proof.
+native_compute.
+reflexivity.
+Qed.
diff --git a/test-suite/success/case_let_param.v b/test-suite/success/case_let_param.v
new file mode 100644
index 0000000000..46d8c26e83
--- /dev/null
+++ b/test-suite/success/case_let_param.v
@@ -0,0 +1,15 @@
+Inductive foo (x := tt) := Foo : forall (y := x), foo.
+
+Definition get (t : foo) := match t with Foo _ y => y end.
+
+Goal get Foo = tt.
+Proof.
+reflexivity.
+Qed.
+
+Goal forall x : foo,
+  match x with Foo _ y => y end = match x with Foo _ _ => tt end.
+Proof.
+intros.
+reflexivity.
+Qed.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 2f676cf9ad..053429a5a9 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -14,8 +14,8 @@ Abort.
 (* Check the combination of at, with and in (see bug #2146) *)
 
 Goal 3=3 -> 3=3. intro H.
-change 3 at 2 with (1+2).
-change 3 at 2 with (1+2) in H |-.
+change 3 with (1+2) at 2.
+change 3 with (1+2) in H at 2 |-.
 change 3 with (1+2) in H at 1 |- * at 1.
 (* Now check that there are no more 3's *)
 change 3 with (1+2) in * || reflexivity.
diff --git a/test-suite/success/let_pattern_mismatch.v b/test-suite/success/let_pattern_mismatch.v
new file mode 100644
index 0000000000..a56a8fff4f
--- /dev/null
+++ b/test-suite/success/let_pattern_mismatch.v
@@ -0,0 +1,18 @@
+(* Weird corner case accepted by the pattern-matching algorithm. Destructuring
+   let-bindings in patterns can actually be shorter than the case they match. *)
+
+Inductive ascii : Set :=
+| Ascii : bool -> bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii.
+
+Definition dummy (a : ascii) : unit :=
+  let (a0,a1,a2,a3,a4,a5,a6,a7) := a in tt.
+
+Goal forall (a : ascii) (H : tt = dummy a), True.
+Proof.
+intros a H.
+unfold dummy in *.
+(* Two bound variables in the pattern, eight in the term. *)
+match goal with
+| H:context [ let (x, y) := ?X in _ ] |- _ => destruct X eqn:?
+end.
+Abort.