7 files changed, 83 insertions, 30 deletions
diff --git a/test-suite/bugs/closed/bug_12806.v b/test-suite/bugs/closed/bug_12806.v
new file mode 100644
index 0000000000..ee221d33a6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12806.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Declare Scope my_scope.
+Delimit Scope my_scope with my_scope.
+
+Notation "###" := tt : my_scope.
+
+Ltac2 Notation "bar" c(open_constr(my_scope)) := c.
+Ltac2 Eval bar ###.
diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v
new file mode 100644
index 0000000000..910537cf11
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13581.v
@@ -0,0 +1,60 @@
+From Coq Require Extraction.
+
+Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }.
+Definition d := Mixin nat tt (fun x => x).
+
+Extraction TestCompile d.
+
+(* Extra tests *)
+
+Record R T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) := Build
+  { g : T0 -> let U:=T0 in U ; h : d = d ; x : nat ; y := x+x }.
+
+Definition r := {| g := (fun x : nat => x) ; h := eq_refl (eq_refl 0) ; x := 0 |}.
+
+Extraction TestCompile r.
+(*
+(** val r0 : nat r **)
+
+let r0 =
+  { g = (fun x0 -> x0); x = O }
+*)
+
+Inductive I T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall d (e:=S d) (h : S d = e), Type :=
+| C : I T a b 0 eq_refl
+| D : J T a b true eq_refl -> I T a b 1 eq_refl
+with J T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall (d:bool) (h:d = true), Type :=
+| E : I T a b 0 eq_refl -> J T a b true eq_refl.
+
+Definition c := D _ _ _ (E _ _ _ (C nat 0 0)).
+
+Extraction TestCompile c.
+
+(*
+(** val c : nat i **)
+
+let c =
+  D (E C)
+*)
+
+CoInductive V T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { k : T; b := c+e ; m : nat; z : option (W nat 0 0 eq_refl) }
+with W T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { l : V nat 0 0 eq_refl }.
+
+CoFixpoint v :=
+  {| k := 0 ; m := 0 ; z := Some w ; |}
+with w := {| l := v |}.
+
+Extraction TestCompile v.
+(*
+(** val v0 : nat v **)
+
+let rec v0 =
+  lazy (Build_V (O, O, (Some w0)))
+
+(** val w0 : nat w **)
+
+and w0 =
+  lazy (Build_W v0)
+*)
diff --git a/test-suite/bugs/closed/bug_1362.v b/test-suite/bugs/closed/bug_1362.v
index 6cafb9f0cd..18b8d743b3 100644
--- a/test-suite/bugs/closed/bug_1362.v
+++ b/test-suite/bugs/closed/bug_1362.v
@@ -1,26 +1,17 @@
 (** Omega is now aware of the bodies of context variables
     (of type Z or nat). *)
 
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z.
 
 Goal let x := 3 in x = 3.
 intros.
-omega.
+lia.
 Qed.
 
 Open Scope nat.
 
 Goal let x := 2 in x = 2.
 intros.
-omega.
+lia.
 Qed.
-
-(** NB: this could be disabled for compatibility reasons *)
-
-Unset Omega UseLocalDefs.
-
-Goal let x := 4 in x = 4.
-intros.
-Fail omega.
-Abort.
diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v
index 0228abbb9b..9f6c8177f6 100644
--- a/test-suite/bugs/closed/bug_1912.v
+++ b/test-suite/bugs/closed/bug_1912.v
@@ -1,6 +1,6 @@
-Require Import Omega.
+Require Import Lia ZArith.
 
 Goal forall x, Z.succ (Z.pred x) = x.
 intros x.
-omega.
+lia.
 Qed.
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 67ecc3087f..2ebbb66758 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -1,5 +1,5 @@
 
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z_scope.
 
 (** bug 4132: omega was using "simpl" either on whole equations, or on
@@ -14,18 +14,18 @@ Lemma foo
   (H : - zxy' <= zxy)
   (H' : zxy' <= x') : - b <= zxy.
 Proof.
-omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
 Qed.
 
 Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
           this might have triggered "index out of bounds" in the past,
           but I never managed to reproduce that in any version,
           even before my fix. *)
 Qed.
 
 Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
           this might have triggered "Failure(occurrence 2)" in the past,
           but I never managed to reproduce that. *)
 Qed.
diff --git a/test-suite/bugs/closed/bug_4717.v b/test-suite/bugs/closed/bug_4717.v
index bd9bac37ef..81bc70d076 100644
--- a/test-suite/bugs/closed/bug_4717.v
+++ b/test-suite/bugs/closed/bug_4717.v
@@ -1,6 +1,6 @@
 (* Omega being smarter on recognizing nat and Z *)
 
-Require Import Omega.
+Require Import Lia ZArith.
 
 Definition nat' := nat.
 
@@ -10,13 +10,13 @@ Theorem le_not_eq_lt : forall (n m:nat),
     n < m.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
 
 Goal forall (x n : nat'), x = x + n - n.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
 
 Open Scope Z_scope.
@@ -29,5 +29,5 @@ Theorem Zle_not_eq_lt : forall n m,
     n < m.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index bad9d64f65..f42e32cf25 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+Require Import Coq.ZArith.BinInt Coq.micromega.Lia.
 
 Set Primitive Projections.
 Record params := { width : Z }.
@@ -10,7 +10,6 @@ Set Printing All.
 Lemma foo : width p = 0%Z -> width p = 0%Z.
   intros.
 
-  assert_succeeds (enough True; [omega|]).
   assert_succeeds (enough True; [lia|]).
 
 (*   H : @eq Z (width p) Z0 *)
@@ -26,12 +25,6 @@ Lemma foo : width p = 0%Z -> width p = 0%Z.
 (*   @eq Z (width p) Z0 *)
 
   assert_succeeds (enough True; [lia|]).
-  (* Tactic failure: <tactic closure> fails. *)
-  (* assert_succeeds (enough True; [omega|]). *)
-  (* Tactic failure: <tactic closure> fails. *)
-
-  (* omega. *)
-  (* Error: Omega can't solve this system *)
 
   lia.
   (* Tactic failure:  Cannot find witness. *)