9 files changed, 150 insertions, 22 deletions
diff --git a/test-suite/bugs/closed/bug_12947.v b/test-suite/bugs/closed/bug_12947.v
new file mode 100644
index 0000000000..baf0579465
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12947.v
@@ -0,0 +1,9 @@
+Require Import BinPos Int63 PArray.
+
+Definition foo (n : positive) :=
+  let a := make 2 0 in
+  let b := Pos.iter (fun b => set b 1 1) a 100000 in
+  let v := get b 0 in
+  Pos.iter (fun v => v + get a 0) v n.
+
+Timeout 5 Time Eval vm_compute in foo 1000000.
diff --git a/test-suite/bugs/closed/bug_13117.v b/test-suite/bugs/closed/bug_13117.v
new file mode 100644
index 0000000000..5db3f9fadc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13117.v
@@ -0,0 +1,23 @@
+
+Class A := {}.
+
+Class B (x:A) := {}.
+Class B' (a:=A) (x:a) := {}.
+
+Fail Definition foo a `{B a} := 0.
+Definition foo a `{B' a} := 0.
+
+Record C (x:A) := {}.
+Existing Class C.
+
+Fail Definition bar a `{C a} := 0.
+
+
+Definition X := Type.
+
+Class Y (x:X) := {}.
+
+Definition before `{Y Set} := 0.
+
+Existing Class X.
+Fail Definition after `{Y Set} := 0.
diff --git a/test-suite/bugs/closed/bug_13129.v b/test-suite/bugs/closed/bug_13129.v
new file mode 100644
index 0000000000..632605ecc7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13129.v
@@ -0,0 +1,58 @@
+From Coq Require Export Morphisms Setoid .
+
+Class Equiv A := equiv: relation A.
+
+Infix "≡" := equiv (at level 70, no associativity).
+Infix "≡@{ A }" := (@equiv A _)
+  (at level 70, only parsing, no associativity).
+
+Notation "(≡)" := equiv (only parsing).
+
+(** Unbundled version *)
+Class Dist A := dist : nat -> relation A.
+
+Notation "x ≡{ n }≡ y" := (dist n x y)
+  (at level 70, n at next level, format "x  ≡{ n }≡  y").
+Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
+  (at level 70, n at next level, only parsing).
+
+Notation NonExpansive f := (forall n, Proper (dist n ==> dist n ==> dist n) f).
+
+Record OfeMixin A `{Equiv A, Dist A} := {
+  mixin_equiv_dist (x y : A) : x ≡ y <-> forall n, x ≡{n}≡ y;
+}.
+
+(** Bundled version *)
+Structure ofeT := OfeT {
+  ofe_car :> Type;
+  ofe_equiv : Equiv ofe_car;
+  ofe_dist : Dist ofe_car;
+  ofe_mixin : OfeMixin ofe_car
+}.
+Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances.
+Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances.
+
+(** Lifting properties from the mixin *)
+Section ofe_mixin.
+  Context {A : ofeT}.
+  Implicit Types x y : A.
+  Lemma equiv_dist x y : x ≡ y <-> forall n, x ≡{n}≡ y.
+  Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed.
+End ofe_mixin.
+
+Axiom _0 : Prop. (* dummy which somehow bothers mangle names *)
+Set Mangle Names.
+
+(** General properties *)
+Section ofe.
+  Context {A : ofeT}.
+
+  Lemma ne_proper_2 {B C : ofeT} (f : A -> B -> C) `{Hf:!NonExpansive f} :
+    Proper ((≡) ==> (≡) ==> (≡)) f.
+  Proof.
+    unfold Proper, respectful.
+    setoid_rewrite equiv_dist.
+    intros.
+    apply Hf;auto.
+  Qed.
+End ofe.
diff --git a/test-suite/micromega/int63.v b/test-suite/micromega/int63.v
new file mode 100644
index 0000000000..20dfa2631e
--- /dev/null
+++ b/test-suite/micromega/int63.v
@@ -0,0 +1,24 @@
+Require Import ZArith ZifyInt63 Lia.
+Require Import Int63.
+
+Open Scope int63_scope.
+
+Goal forall (x:int), 0 <= x = true.
+Proof. lia. Qed.
+
+Goal max_int = 9223372036854775807.
+Proof. lia. Qed.
+
+Goal digits = 63.
+Proof. lia. Qed.
+
+Goal wB = (2^63)%Z.
+Proof. lia. Qed.
+
+Goal forall x y, x + y <= max_int = true.
+Proof. lia. Qed.
+
+Goal forall x, x <> 0 -> x / x = 1.
+Proof.
+  nia.
+Qed.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index da2fc90fc3..01564e7f25 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -178,3 +178,6 @@ match N with
 | _ => Node
 end
      : Tree -> Tree
+File "stdin", line 253, characters 4-5:
+Warning: Unused variable B catches more than one case.
+[unused-pattern-matching-variable,pattern-matching]
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 262ec2b677..2d8a8b359c 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -242,3 +242,15 @@ end.
 Print stray.
 
 End Bug11231.
+
+Module Wish12762.
+
+Inductive foo := a | b | c.
+
+Definition bar (f : foo) :=
+  match f with
+  | a => 0
+  | B => 1
+  end.
+
+End Wish12762.
diff --git a/test-suite/output/DependentInductionErrors.out b/test-suite/output/DependentInductionErrors.out
new file mode 100644
index 0000000000..4a83375f6f
--- /dev/null
+++ b/test-suite/output/DependentInductionErrors.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Tactic failure: To use dependent destruction, first [Require Import Coq.Program.Equality.].
+The command has indeed failed with message:
+Tactic failure: To use dependent induction, first [Require Import Coq.Program.Equality.].
diff --git a/test-suite/output/DependentInductionErrors.v b/test-suite/output/DependentInductionErrors.v
new file mode 100644
index 0000000000..2fce00f9fd
--- /dev/null
+++ b/test-suite/output/DependentInductionErrors.v
@@ -0,0 +1,17 @@
+Theorem foo (b:bool) : b = true \/ b = false.
+Proof.
+  Fail dependent destruction b.
+  Fail dependent induction b.
+Abort.
+
+From Coq Require Import Program.Equality.
+
+Theorem foo_with_destruction (b:bool) : b = true \/ b = false.
+Proof.
+  dependent destruction b; auto.
+Qed.
+
+Theorem foo_with_induction (b:bool) : b = true \/ b = false.
+Proof.
+  dependent induction b; auto.
+Qed.
diff --git a/test-suite/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v
deleted file mode 100644
index 172a118cc7..0000000000
--- a/test-suite/primitive/arrays/reroot.v
+++ /dev/null
@@ -1,22 +0,0 @@
-From Coq Require Import Int63 PArray.
-
-Open Scope array_scope.
-
-Definition t : array nat := [| 1; 5; 2 | 4 |].
-Definition t' : array nat := PArray.reroot t.
-
-Definition foo1 := (eq_refl : t'.[1] = 5).
-Definition foo2 := (eq_refl 5 <: t'.[1] = 5).
-Definition foo3 := (eq_refl 5 <<: t'.[1] = 5).
-Definition x1 := Eval compute in t'.[1].
-Definition foo4 := (eq_refl : x1 = 5).
-Definition x2 := Eval cbn in t'.[1].
-Definition foo5 := (eq_refl : x2 = 5).
-
-Definition foo6 := (eq_refl : t.[1] = 5).
-Definition foo7 := (eq_refl 5 <: t.[1] = 5).
-Definition foo8 := (eq_refl 5 <<: t.[1] = 5).
-Definition x3 := Eval compute in t.[1].
-Definition foo9 := (eq_refl : x3 = 5).
-Definition x4 := Eval cbn in t.[1].
-Definition foo10 := (eq_refl : x4 = 5).