12 files changed, 146 insertions, 58 deletions

diff --git a/test-suite/bugs/closed/bug_11866.v b/test-suite/bugs/closed/bug_11866.v
new file mode 100644
index 0000000000..5a47f3833e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11866.v
@@ -0,0 +1,43 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Notation "ex0" x(tactic(0)) := ().
+Ltac2 Notation "ex1" x(tactic(1)) := ().
+Ltac2 Notation "ex2" x(tactic(2)) := ().
+Ltac2 Notation "ex3" x(tactic(3)) := ().
+Ltac2 Notation "ex4" x(tactic(4)) := ().
+Ltac2 Notation "ex5" x(tactic(5)) := ().
+Ltac2 Notation "ex6" x(tactic(6)) := ().
+
+Ltac2 Notation ":::0" x(tactic) "+0" y(tactic) : 0 := ().
+Ltac2 Notation ":::1" x(tactic) "+1" y(tactic) : 1 := ().
+Ltac2 Notation ":::2" x(tactic) "+2" y(tactic) : 2 := ().
+Ltac2 Notation ":::3" x(tactic) "+3" y(tactic) : 3 := ().
+Ltac2 Notation ":::4" x(tactic) "+4" y(tactic) : 4 := ().
+Ltac2 Notation ":::5" x(tactic) "+5" y(tactic) : 5 := ().
+Ltac2 Notation ":::6" x(tactic) "+6" y(tactic) : 6 := ().
+Fail Ltac2 Notation ":::7" x(tactic) "+7" y(tactic) : 7 := ().
+Goal True.
+  ex0 :::0 0 +0 0.
+  ex1 :::0 0 +0 0.
+  (*ex2 :::0 0 +0 0.*) (* fails with an anomaly, cf COQBUG(https://github.com/coq/coq/issues/12807) *)
+  (*ex3 :::0 0 +0 0.*)
+  ex4 :::0 0 +0 0.
+  ex5 :::0 0 +0 0.
+  ex6 :::0 0 +0 0.
+
+  ex0 :::1 0 +1 0.
+  ex1 :::1 0 +1 0.
+  (*ex2 :::1 0 +1 0.*)
+  (*ex3 :::1 0 +1 0.*)
+  ex4 :::1 0 +1 0.
+  ex5 :::1 0 +1 0.
+  ex6 :::1 0 +1 0.
+
+  ex0 :::6 0 +6 0.
+  ex1 :::6 0 +6 0.
+  (*ex2 :::6 0 +6 0.*)
+  (*ex3 :::6 0 +6 0.*)
+  ex4 :::6 0 +6 0.
+  ex5 :::6 0 +6 0.
+  ex6 :::6 0 +6 0.
+Abort.
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_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/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_3468.v b/test-suite/bugs/closed/bug_3468.v
index 6ff394bca6..8d7d97d7aa 100644
--- a/test-suite/bugs/closed/bug_3468.v
+++ b/test-suite/bugs/closed/bug_3468.v
@@ -26,4 +26,5 @@ Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope.
 Definition test := (& (@4))%my.
 
 (* Check inconsistent scopes *)
+Set Warnings "+inconsistent-scopes".
 Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing).
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. *)
diff --git a/test-suite/bugs/opened/bug_1615.v b/test-suite/bugs/opened/bug_1615.v
deleted file mode 100644
index c045335410..0000000000
--- a/test-suite/bugs/opened/bug_1615.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Require Import Omega.
-
-Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
-Proof.
-  intros. omega.
-Qed.
-
-Lemma foo' : forall n m : nat, n <=  n + n * m.
-Proof.
-  intros. Fail omega.
-Abort.
diff --git a/test-suite/bugs/opened/bug_6602.v b/test-suite/bugs/opened/bug_6602.v
deleted file mode 100644
index 3690adf90a..0000000000
--- a/test-suite/bugs/opened/bug_6602.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Omega.
-
-Lemma test_nat:
-  forall n, (5 + pred n <= 5 + n).
-Proof.
-  intros.
-  zify.
-  omega.
-Qed.
-
-Lemma test_N:
-  forall n, (5 + N.pred n <= 5 + n)%N.
-Proof.
-  intros.
-  zify.
-  omega.
-Qed.