3 files changed, 102 insertions, 29 deletions

diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index aa439fae12..f166a53256 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -7,21 +7,21 @@ The convention is:
 Constant foo with implicit arguments and scopes used in a term or a pattern:
 
        foo      do not deactivate further arguments and scopes
-       @foo     deactivates further arguments and scopes
-       (foo x)  deactivates further arguments and scopes
-       (@foo x) deactivates further arguments and scopes
+       @foo     deactivate further arguments and scopes
+       (foo x)  deactivate further arguments and scopes
+       (@foo x) deactivate further arguments and scopes
 
 Notations binding to foo:
 
 #   := foo      do not deactivate further arguments and scopes
-#   := @foo     deactivates further arguments and scopes
-# x := foo x    deactivates further arguments and scopes
-# x := @foo x   deactivates further arguments and scopes
+#   := @foo     deactivate further arguments and scopes
+# x := foo x    do not deactivate further arguments and scopes
+# x := @foo x   do not deactivate further arguments and scopes
 
 Abbreviations binding to foo:
 
 f   := foo      do not deactivate further arguments and scopes
-f   := @foo     deactivates further arguments and scopes
+f   := @foo     deactivate further arguments and scopes
 f x := foo x    do not deactivate further arguments and scopes
 f x := @foo x   do not deactivate further arguments and scopes
 *)
@@ -62,18 +62,18 @@ Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 
-(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 5. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
-Check # 0 _ 0%bool 0%bool : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+Check # 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with # 0 y 0 => 2 | _ => 1 end.
 
-(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
+(* 6. Non-@id notations inherit implicit arguments to be inserted and scopes to be used *)
 Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
-Check ## 0%bool _ 0%bool 0%bool : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check ## 0%bool 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ## 0%bool y 0 => 2 | _ => 1 end.
 
 (* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
 Notation "###" := (@pair') (at level 0).
@@ -86,10 +86,10 @@ Notation "####" := pair' (at level 0).
 Check #### 0 0 0 : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 
-(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+(* 9. Non-@id notations inherit implicit arguments and scopes *)
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
-Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
-Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+Check ##### 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ##### 0 y 0 => 2 | _ => 1 end.
 
 (* 10. Check computation of binding variable through other notations *)
 (* it should be detected as binding variable and the scopes not being checked *)
@@ -172,3 +172,25 @@ Notation "#" := 0 (only printing).
 Print Visibility.
 
 End Bug10750.
+
+Module M18.
+
+  Module A.
+    Module B.
+    Infix "+++" := Nat.add (at level 70).
+    End B.
+  End A.
+Import A.
+(* Check that the notation in module B is not visible *)
+Infix "+++" := Nat.add (at level 80).
+
+End M18.
+
+Module InheritanceArgumentScopes.
+
+Axiom p : forall (A:Type) (b:nat), A = A /\ b = b.
+Check fun A n => p (A * A) (n * n). (* safety check *)
+Notation q := @p.
+Check fun A n => q (A * A) (n * n). (* check that argument scopes are propagated *)
+
+End InheritanceArgumentScopes.
diff --git a/test-suite/success/NotationsAndLtac.v b/test-suite/success/NotationsAndLtac.v
new file mode 100644
index 0000000000..f3ec1916dc
--- /dev/null
+++ b/test-suite/success/NotationsAndLtac.v
@@ -0,0 +1,52 @@
+(* Test that adding notations that overlap with the tactic grammar does not
+* interfere with Ltac parsing. *)
+
+Module test1.
+  Notation "x [ y ]" := (fst (id x, id y)) (at level 11).
+
+  Goal True \/ (exists x : nat, True /\ True) -> True.
+  Proof.
+  intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]].
+  Qed.
+End test1.
+
+Module test2.
+  Notation "x [ y ]" := (fst (id x, id y)) (at level 100).
+  Goal True \/ (exists x : nat, True /\ True) -> True.
+  Proof.
+  intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]].
+  Qed.
+End test2.
+
+Module test3.
+  Notation "x [ y ]" := (fst (id x, id y)) (at level 1).
+  Goal True \/ (exists x : nat, True /\ True) -> True.
+  Proof.
+  intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]].
+  Qed.
+End test3.
+
+Module test1'.
+  Notation "x [ [ y ] ] " := (fst (id x, id y)) (at level 11).
+
+  Goal True \/ (exists x : nat, True /\ True) -> True.
+  Proof.
+  intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]].
+  Qed.
+End test1'.
+
+Module test2'.
+  Notation "x [ [ y ] ]" := (fst (id x, id y)) (at level 100).
+  Goal True \/ (exists x : nat, True /\ True) -> True.
+  Proof.
+  intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]].
+  Qed.
+End test2'.
+
+Module test3'.
+  Notation "x [ [ y ] ]" := (fst (id x, id y)) (at level 1).
+  Goal True \/ (exists x : nat, True /\ True) -> True.
+  Proof.
+  intros [|[a [y z]]]; [idtac|idtac]; try solve [eauto | trivial; [trivial]].
+  Qed.
+End test3'.
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 651247937d..e2b4694fff 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,23 +1,22 @@
-Module Att.
-  #[uniform] Inductive list (A : Type) :=
-  | nil : list
-  | cons : A -> list -> list.
-  Check (list : Type -> Type).
-  Check (cons : forall A, A -> list A -> list A).
-End Att.
-
 Set Uniform Inductive Parameters.
 
 Inductive list (A : Type) :=
-| nil : list
-| cons : A -> list -> list.
+  | nil : list
+  | cons : A -> list -> list.
 Check (list : Type -> Type).
 Check (cons : forall A, A -> list A -> list A).
 
 Inductive list2 (A : Type) (A' := prod A A) :=
-| nil2 : list2
-| cons2 : A' -> list2 -> list2.
+  | nil2 : list2
+  | cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
 
-#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)).
+Inductive list3 | A := nil3 | cons3 : A -> list3 (A * A)%type -> list3 A.
+
+Unset Uniform Inductive Parameters.
+
+Inductive list4 A | := nil4 | cons4 : A -> list4 -> list4.
+
+Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop
+  := Acc_in : (forall y, R y x -> Acc y) -> Acc x.