5 files changed, 173 insertions, 3 deletions
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/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/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v
new file mode 100644
index 0000000000..2a5e083d56
--- /dev/null
+++ b/test-suite/success/Discriminate_HoTT.v
@@ -0,0 +1,89 @@
+(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *)
+
+(* This file tests the discriminate tactic compatibility with HoTT.
+   The first part of the file will setup a mini HoTT environment.
+   Afterwards a number of tests are performed. The tests are basically
+   copied from the Discriminate.v test file. *)
+
+Unset Elimination Schemes.
+
+Set Universe Polymorphism.
+
+Declare ML Module "ltac_plugin".
+
+Global Set Default Proof Mode "Classic".
+
+Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200).
+
+Cumulative Variant paths {A} (a:A) : A -> Type
+  := idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+Arguments paths_ind [A] a P f y p.
+
+Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity).
+Notation "x = y" := (x = y :>_) (at level 70, no associativity).
+
+Register paths as core.identity.type.
+Register idpath as core.identity.refl.
+Register paths_ind as core.identity.ind.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Arguments inverse {A x y} p : simpl nomatch.
+Register inverse as core.identity.sym.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Arguments concat {A x y z} p q : simpl nomatch.
+Register concat as core.identity.trans.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Arguments ap {A B} f {x y} p.
+Register ap as core.identity.congr.
+
+Variant Empty : Type :=.
+
+Register Empty as core.False.type.
+
+Variant Unit : Type := tt.
+
+Register Unit as core.True.type.
+Register tt as core.True.I.
+
+Variant Bool : Type := true | false.
+
+Inductive nat : Type := O | S (n:nat).
+
+(*********** Test discriminate tactic below. ***************)
+
+Goal O = S O -> Empty.
+ discriminate 1.
+Qed.
+
+Goal forall H : O = S O, H = H.
+ discriminate H.
+Qed.
+
+Goal O = S O -> Unit.
+intros. discriminate H. Qed.
+Goal O = S O -> Unit.
+intros. Ltac g x := discriminate x. g H. Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> Unit.
+intros.
+try discriminate (H O) || exact tt.
+Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> Unit.
+intros. ediscriminate (H O). instantiate (1:=O). Abort.
+
+(* Check discriminate on types with local definitions *)
+
+Inductive A := B (T := Unit) (x y : Bool) (z := x).
+Goal forall x y, B x true = B y false -> Empty.
+discriminate.
+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/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.