7 files changed, 148 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v
deleted file mode 100644
index f238086633..0000000000
--- a/test-suite/bugs/closed/bug_4798.v
+++ /dev/null
@@ -1,5 +0,0 @@
-(* DO NOT MODIFY THIS FILE DIRECTLY *)
-(* It is autogenerated by dev/tools/update-compat.py. *)
-Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.8").
-Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/bugs/closed/bug_8725.v b/test-suite/bugs/closed/bug_8725.v
new file mode 100644
index 0000000000..c888b9e96d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8725.v
@@ -0,0 +1,2 @@
+Set Warnings "+local-declaration".
+Fail Let foo : True.
diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v
index 21cd770cbb..cd594c660f 100644
--- a/test-suite/bugs/closed/bug_9166.v
+++ b/test-suite/bugs/closed/bug_9166.v
@@ -1,8 +1,7 @@
-(* DO NOT MODIFY THIS FILE DIRECTLY *)
-(* It is autogenerated by dev/tools/update-compat.py. *)
 Set Warnings "+deprecated".
 
-Notation bar := option (compat "8.8").
+#[deprecated(since = "X", note = "Y")]
+Notation bar := option.
 
 Definition foo (x: nat) : nat :=
   match x with
diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v
new file mode 100644
index 0000000000..3d2a875e38
--- /dev/null
+++ b/test-suite/ltac2/notations.v
@@ -0,0 +1,24 @@
+From Ltac2 Require Import Ltac2.
+From Coq Require Import ZArith String List.
+
+Open Scope Z_scope.
+
+Check 1 + 1 : Z.
+
+Ltac2 Notation "ex" arg(constr(nat,Z)) := arg.
+
+Check (1 + 1)%nat%Z = 1%nat.
+
+Lemma two : nat.
+  refine (ex (1 + 1)).
+Qed.
+
+Import ListNotations.
+Close Scope list_scope.
+
+Ltac2 Notation "sl" arg(constr(string,list)) := arg.
+
+Lemma maybe : list bool.
+Proof.
+  refine (sl ["left" =? "right"]).
+Qed.
diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v
new file mode 100644
index 0000000000..22fb09526d
--- /dev/null
+++ b/test-suite/success/LocalDefinition.v
@@ -0,0 +1,53 @@
+(* Test consistent behavior of Local Definition (#8722) *)
+
+(* Test consistent behavior of Local Definition wrt Admitted *)
+
+Module TestAdmittedVisibility.
+  Module A.
+    Let a1 : nat. Admitted. (* Suppose to behave like a "Local Definition" *)
+    Local Definition b1 : nat. Admitted. (* Told to be a "Local Definition" *)
+    Local Definition c1 := 0.
+    Local Parameter d1 : nat.
+    Section S.
+      Let a2 : nat. Admitted. (* Told to be turned into a toplevel assumption *)
+      Local Definition b2 : nat. Admitted. (* Told to be a "Local Definition" *)
+      Local Definition c2 := 0.
+      Local Parameter d2 : nat.
+    End S.
+  End A.
+  Import A.
+  Fail Check a1. (* used to be accepted *)
+  Fail Check b1. (* used to be accepted *)
+  Fail Check c1.
+  Fail Check d1.
+  Fail Check a2. (* used to be accepted *)
+  Fail Check b2. (* used to be accepted *)
+  Fail Check c2.
+  Fail Check d2.
+End TestAdmittedVisibility.
+
+(* Test consistent behavior of Local Definition wrt automatic declaration of instances *)
+
+Module TestVariableAsInstances.
+  Module Test1.
+    Set Typeclasses Axioms Are Instances.
+    Class U.
+    Local Parameter b : U.
+    Definition testU := _ : U. (* _ resolved *)
+
+    Class T.
+    Variable a : T.  (* warned to be the same as "Local Parameter" *)
+    Definition testT := _ : T. (* _ resolved *)
+  End Test1.
+
+  Module Test2.
+    Unset Typeclasses Axioms Are Instances.
+    Class U.
+    Local Parameter b : U.
+    Fail Definition testU := _ : U. (* _ unresolved *)
+
+    Class T.
+    Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
+    Fail Definition testT := _ : T. (* used to succeed *)
+  End Test2.
+End TestVariableAsInstances.
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
new file mode 100644
index 0000000000..d313ba0aa4
--- /dev/null
+++ b/test-suite/success/NotationDeprecation.v
@@ -0,0 +1,62 @@
+Module Syndefs.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation foo := Prop.
+
+Notation bar := Prop (compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation zar := Prop (compat "8.8").
+
+Check foo.
+Check bar.
+
+Set Warnings "+deprecated".
+
+Fail Check foo.
+Fail Check bar.
+
+End Syndefs.
+
+Module Notations.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation "!!" := Prop.
+
+Notation "##" := Prop (compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Notation "**" := Prop (compat "8.8").
+
+Check !!.
+Check ##.
+
+Set Warnings "+deprecated".
+
+Fail Check !!.
+Fail Check ##.
+
+End Notations.
+
+Module Infix.
+
+#[deprecated(since = "8.8", note = "Do not use.")]
+Infix "!!" := plus (at level 1).
+
+Infix "##" := plus (at level 1, compat "8.8").
+
+Fail
+#[deprecated(since = "8.8", note = "Do not use.")]
+Infix "**" := plus (at level 1, compat "8.8").
+
+Check (_ !! _).
+Check (_ ## _).
+
+Set Warnings "+deprecated".
+
+Fail Check (_ !! _).
+Fail Check (_ ## _).
+
+End Infix.
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 0951c5c8d4..ae834e7696 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
 Proof.
   do 2 dup.
   - repeat split.
-    2, 4-99, 100-3:idtac.
+    Fail 7:idtac.
+    Fail 2-1:idtac.
+    1,2,4-6:idtac.
     2-5:exact One.
     par:exact Zero.
   - repeat split.
     3-6:swap 1 4.
     1-5:swap 1 5.
-    0-4:exact One.
+    1-4:exact One.
     all:exact Zero.
   - repeat split.
     1, 3:exact Zero.
@@ -34,7 +36,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; only 1-2 : repeat idtac.
+  intros y.
   1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.