14 files changed, 154 insertions, 23 deletions

diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/bug_9490.v
new file mode 100644
index 0000000000..a5def40c49
--- /dev/null
+++ b/test-suite/bugs/bug_9490.v
@@ -0,0 +1,9 @@
+Declare Custom Entry with_pattern.
+Declare Custom Entry M_branch.
+Notation "'with' | p1 | .. | pn 'end'" :=
+  (cons p1 (.. (cons pn nil) ..))
+  (in custom with_pattern at level 91, p1 custom M_branch at level 202, pn custom M_branch at level 202).
+Notation "'bla'" := I (in custom M_branch at level 202).
+Notation "'[use_with'  l  ]" := (l) (at level 0, l custom with_pattern at level 91).
+Check [use_with with | bla end].
+Check [use_with with | bla | bla end].
diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/bug_9532.v
new file mode 100644
index 0000000000..d198d45f2f
--- /dev/null
+++ b/test-suite/bugs/bug_9532.v
@@ -0,0 +1,12 @@
+Declare Custom Entry atom.
+Notation "1" := tt (in custom atom).
+Notation "atom:( s )" := s (s custom atom).
+
+Declare Custom Entry expr.
+Notation "expr:( s )" := s (s custom expr).
+Notation "( x , y , .. , z )" :=  (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..))
+  (in custom expr at level 0, x custom atom, y custom atom, z custom atom).
+
+Check atom:(1).
+Check expr:((1,1)).
+Check expr:((1,1,1)).
diff --git a/test-suite/bugs/closed/bug_10298.v b/test-suite/bugs/closed/bug_10298.v
new file mode 100644
index 0000000000..ad4778cc36
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10298.v
@@ -0,0 +1,35 @@
+Set Implicit Arguments.
+
+Generalizable Variables A.
+
+Parameter val : Type.
+
+Class Enc (A:Type) :=
+  make_Enc { enc : A -> val }.
+
+Global Instance Enc_dummy : Enc unit.
+Admitted.
+
+Definition FORM := forall A (EA:Enc A) (Q:A->Prop), Prop.
+
+Axiom FORM_intro : forall F : FORM, F unit Enc_dummy (fun _ : unit => True).
+
+Definition IDF (F:FORM) : FORM := F.
+
+Parameter ID : forall (G:Prop), G -> G.
+
+Parameter EID : forall A (EA:Enc A) (F:FORM) (Q:A->Prop),
+  F _ _ Q ->
+  F _ _ Q.
+
+Lemma bla : forall F,
+  (forall A (EA:Enc A), IDF F EA (fun (X:A) => True) -> True) ->
+  True.
+Proof.
+  intros F M.
+  notypeclasses refine (M _ _ _).
+  notypeclasses refine (EID _ _ _ _).
+  eapply (ID _).
+  Unshelve.
+  + apply FORM_intro.
+Qed.
diff --git a/test-suite/bugs/closed/bug_10504.v b/test-suite/bugs/closed/bug_10504.v
new file mode 100644
index 0000000000..6e66a6a90a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10504.v
@@ -0,0 +1,14 @@
+Inductive any_list {A} :=
+| nil : @any_list A
+| cons : forall X, A -> @any_list X -> @any_list A.
+
+Arguments nil {A}.
+Arguments cons {A X}.
+
+Notation "[]" := (@nil Type).
+Notation "hd :: tl" := (cons hd tl).
+
+Definition xs := true :: 2137 :: false :: 0 :: [].
+Fail Definition ys := xs :: xs.
+
+(* Goal ys = ys. produced an anomaly "Unable to handle arbitrary u+k <= v constraints" *)
diff --git a/test-suite/bugs/closed/bug_10762.v b/test-suite/bugs/closed/bug_10762.v
new file mode 100644
index 0000000000..d3991d4d38
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10762.v
@@ -0,0 +1,30 @@
+
+Set Implicit Arguments.
+
+Generalizable Variables A B.
+Parameter val: Type.
+
+Class Enc (A:Type) : Type :=
+  make_Enc { enc : A -> val }.
+
+Hint Mode Enc + : typeclass_instances.
+
+Parameter bar : forall A (EA:Enc A), EA = EA.
+
+Parameter foo : forall (P:Prop),
+   P ->
+   P = P ->
+   True.
+
+Parameter id : forall (P:Prop),
+  P -> P.
+
+  Check enc.
+
+  Lemma test : True.
+  eapply foo; [ eapply bar | apply id]. apply id.
+  (* eapply bar introduces an unresolved typeclass evar that is no longer
+     a candidate after the application (eapply should leave typeclass goals shelved).
+     We ensure that this happens also _across_ goals in `[ | ]` and not only at `.`..
+      *)
+  Abort.
diff --git a/test-suite/bugs/closed/bug_11039.v b/test-suite/bugs/closed/bug_11039.v
new file mode 100644
index 0000000000..f02a3ef177
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11039.v
@@ -0,0 +1,26 @@
+(* this bug was a proof of False *)
+
+(* when we require template poly Coq recognizes that it's not allowed *)
+Fail #[universes(template)]
+  Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A.
+
+(* variants with letin *)
+Fail #[universes(template)]
+ Inductive foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A.
+
+Fail #[universes(template)]
+ Record foo@{i}  (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }.
+
+
+(* no implicit template poly, no explicit universe annotations *)
+Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty.
+Arguments nonempty {_}.
+
+Fail Check foo nat : Type@{foo.u0}.
+(* template poly didn't activate *)
+
+Definition U := Type.
+Definition A : U := foo nat.
+
+Fail Definition down : U -> A := fun u => bar nat u nonempty.
+(* this is the one where it's important that it fails *)
diff --git a/test-suite/bugs/closed/bug_2083.v b/test-suite/bugs/closed/bug_2083.v
index f33e96cea6..40fda71e66 100644
--- a/test-suite/bugs/closed/bug_2083.v
+++ b/test-suite/bugs/closed/bug_2083.v
@@ -13,15 +13,15 @@ Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
         error
   end.
 
-Require Import Omega.
+Require Import Lia.
 
-Solve Obligations with program_simpl ; auto with *; try omega.
+Solve Obligations with program_simpl ; auto with *; lia.
 
 Next Obligation.
-  apply H. simpl. omega.
+  apply H. simpl. lia.
 Defined.
 
 Next Obligation.
-  case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
+  case (le_lt_dec p i) ; intros. assert(i = p) by lia. subst.
   revert H0. clear_subset_proofs. auto.
   apply H. simpl. assumption. Defined.
diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v
index 915cfcac27..b21a4d939c 100644
--- a/test-suite/bugs/closed/bug_3652.v
+++ b/test-suite/bugs/closed/bug_3652.v
@@ -1,6 +1,7 @@
 Require Setoid.
 Require ZArith.
 Import ZArith.
+Require Import Lia.
 
 Inductive Erasable(A : Set) : Prop :=
   erasable: A -> Erasable A.
@@ -87,12 +88,12 @@ Proof.
     unfold zotval.
     unfold mp2a1s.
     ring_simplify'.
-    replace 2 with (2*1) at 2 7 by omega.
+    replace 2 with (2*1) at 2 7 by lia.
     rewrite <-?Z.mul_assoc.
     rewrite <-?Z.mul_add_distr_l.
     rewrite <-Z.mul_sub_distr_l.
-    rewrite Z.mul_cancel_l by omega.
-    replace 1 with (2-1) at 1 by omega.
+    rewrite Z.mul_cancel_l by lia.
+    replace 1 with (2-1) at 1 by lia.
     rewrite Z.add_sub_assoc.
     rewrite Z.sub_cancel_r.
     Unshelve.
diff --git a/test-suite/bugs/closed/bug_4280.v b/test-suite/bugs/closed/bug_4280.v
index fd7897509e..31524e5dcf 100644
--- a/test-suite/bugs/closed/bug_4280.v
+++ b/test-suite/bugs/closed/bug_4280.v
@@ -1,11 +1,11 @@
-Require Import ZArith.
+Require Import ZArith Lia.
 Require Import Eqdep_dec.
 Local Open Scope Z_scope.
 
 Definition t := { n: Z | n > 1 }.
 
 Program Definition two : t := 2.
-Next Obligation. omega. Qed.
+Next Obligation. lia. Qed.
 
 Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
   if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v
index f1bce04451..1ad84f9bb5 100644
--- a/test-suite/bugs/closed/bug_4306.v
+++ b/test-suite/bugs/closed/bug_4306.v
@@ -1,7 +1,7 @@
 Require Import List.
 Require Import Arith.
 Require Import Recdef.
-Require Import Omega.
+Require Import Lia.
 
 Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
   match xys with
@@ -14,9 +14,7 @@ Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
                               end
   end.
 Proof.
-  intros; simpl; omega.
-  intros; simpl; omega.
-  intros; simpl; omega.
+  all: simpl; lia.
 Qed.
 
 Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v
index 7685552725..0c26d4de32 100644
--- a/test-suite/bugs/closed/bug_4456.v
+++ b/test-suite/bugs/closed/bug_4456.v
@@ -10,7 +10,7 @@ Tactic Notation "admit" := case proof_admitted.
 
 Require Coq.Program.Program.
 Require Coq.Strings.String.
-Require Coq.omega.Omega.
+Require Coq.micromega.Lia.
 Module Export Fiat_DOT_Common.
 Module Export Fiat.
 Module Common.
@@ -489,7 +489,8 @@ Defined.
   End app.
 
 Import Coq.Lists.List.
-Import Coq.omega.Omega.
+Import Coq.Arith.Arith.
+Import Coq.micromega.Lia.
 Import Fiat_DOT_Common.Fiat.Common.
 Import Fiat.Parsers.ContextFreeGrammar.Valid.
 Local Open Scope string_like_scope.
@@ -585,8 +586,8 @@ Defined.
               | _ => discriminate
               | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z))
               | _ => solve [ eauto with nocore ]
-              | _ => solve [ apply Min.min_case_strong; omega ]
-              | _ => omega
+              | _ => solve [ apply Min.min_case_strong; lia ]
+              | _ => lia
               | [ H : production_valid (_::_) |- _ ]
                 => let H' := fresh in
                    pose proof H as H';
diff --git a/test-suite/bugs/closed/bug_4852.v b/test-suite/bugs/closed/bug_4852.v
index e2e00f05d3..cdc8cd8b20 100644
--- a/test-suite/bugs/closed/bug_4852.v
+++ b/test-suite/bugs/closed/bug_4852.v
@@ -2,7 +2,7 @@
 
 Require Import Coq.Lists.List.
 Import ListNotations.
-Require Import Omega.
+Require Import Lia.
 
 Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.
 
@@ -16,7 +16,7 @@ Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) :=
 
 Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws.
 
-Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega.
+Ltac solve_nat := autorewrite with app_rws in *; cbn in *; lia.
 
 Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'").
 
diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v
index 27cb731151..89410047b2 100644
--- a/test-suite/bugs/opened/bug_1596.v
+++ b/test-suite/bugs/opened/bug_1596.v
@@ -1,7 +1,7 @@
 Require Import Relations.
 Require Import FSets.
 Require Import Arith.
-Require Import Omega.
+Require Import Lia.
 
 Set Keyed Unification.
 
@@ -147,14 +147,14 @@ Module MessageSpi.
     Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
       unfold lt.
       induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
-      omega.
+      lia.
     Qed.
 
     Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
       unfold eq;unfold lt.
       induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
 H0);injection H0;intros.
-      elim (lt_irrefl n);try omega.
+      elim (lt_irrefl n); lia.
     Qed.
 
     Definition compare : forall (x y:t),(Compare lt eq x y).
diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v
index c479158877..f0e5d71811 100644
--- a/test-suite/bugs/opened/bug_3357.v
+++ b/test-suite/bugs/opened/bug_3357.v
@@ -1,4 +1,9 @@
-Notation D1 := (forall {T : Type} ( x : T ) , Type).
+(* See discussion in #668 for whether manual implicit arguments should
+   be allowed in notations or not *)
+
+Set Warnings "+syntax".
+
+Fail Notation D1 := (forall {T : Type} ( x : T ) , Type).
 
 Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
 Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33: