12 files changed, 222 insertions, 11 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 623ca316c9..a9bed49922 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -120,14 +120,14 @@ where
 letpair x [1] = {0};
 return (1, 2, 3, 4)
      : nat * nat * nat * nat
-{{ 1 | 1 // 1 }}
-     : nat
-!!! _ _ : nat, True
-     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ((*1).2).3
      : nat
 *(1.2)
      : nat
+{{ 1 | 1 // 1 }}
+     : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
 ! '{{x, y}}, x.y = 0
      : Prop
 exists x : nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index ce97d909a7..04a91c14d9 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" :=
   (let x:=a in ( .. (b0,b1) .., b2)).
 Check letpair x [1] = {0}; return (1,2,3,4).
 
+(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
+
+Notation "* x" := (id x) (only printing, at level 15, format "* x").
+Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
+Check (((id 1) + 2) + 3).
+Check (id (1 + 2)).
+
 (* Test spacing in #5569 *)
 
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
@@ -191,13 +198,6 @@ Check 1+1+1.
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
 Check !!! (x y:nat), True.
 
-(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
-
-Notation "* x" := (id x) (only printing, at level 15, format "* x").
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y").
-Check (((id 1) + 2) + 3).
-Check (id (1 + 2)).
-
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)
 Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index a6fd39c29b..86c4b3cccc 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -179,3 +179,21 @@ Found an inductive type while a pattern was expected.
      : Prop
 !!!! (nat, id), nat = true /\ id = false
      : Prop
+∀ x : nat, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₁ x, x = 0
+     : Prop
+∀₂ x y, x + y = 0
+     : Prop
+((1, 2))
+     : nat * nat
+%% [x == 1]
+     : Prop
+%%% [1]
+     : Prop
+[[2]]
+     : nat * nat
+%%%
+     : Type
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 0731819bba..6af192ea82 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -414,3 +414,76 @@ Module P.
   End NotationBinderNotMixedWithTerms.
 
 End P.
+
+Module MorePrecise1.
+
+(* A notation with limited iteration is strictly more precise than a
+   notation with unlimited iteration *)
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₁ z , P" := (forall z, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+
+Notation "∀₂ y x , P" := (forall y x, P)
+  (at level 200, right associativity) : type_scope.
+
+Check forall x, x = 0.
+Check forall x y, x + y = 0.
+
+Notation "(( x , y ))" := (x,y) : core_scope.
+
+Check ((1,2)).
+
+End MorePrecise1.
+
+Module MorePrecise2.
+
+(* Case of a bound binder *)
+Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60).
+
+(* Case of an internal binder *)
+Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0).
+
+(* Check that the two previous notations are indeed finer *)
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀'  x  ..  y ']' ,  '/' P ']'").
+
+Check %% [x == 1].
+Check %%% [1].
+
+Notation "[[ x ]]" := (pair 1 x).
+
+Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z).
+Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y).
+
+(* Check which is finer *)
+Check [[ 2 ]].
+
+End MorePrecise2.
+
+Module MorePrecise3.
+
+(* This is about a binder not bound in a notation being strictly more
+   precise than a binder bound in the notation (since the notation
+   applies - a priori - stricly less often) *)
+
+Notation "%%%" := (forall x, x) (at level 0).
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'").
+
+Check %%%.
+
+End MorePrecise3.
diff --git a/test-suite/output/attributes.out b/test-suite/output/attributes.out
new file mode 100644
index 0000000000..25572ee2aa
--- /dev/null
+++ b/test-suite/output/attributes.out
@@ -0,0 +1,11 @@
+The command has indeed failed with message:
+Attribute for canonical specified twice.
+The command has indeed failed with message:
+key 'polymorphic' has been already set.
+The command has indeed failed with message:
+Invalid value 'foo' for key polymorphic
+use one of {yes, no}
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead.
+The command has indeed failed with message:
+Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead.
diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v
new file mode 100644
index 0000000000..aef05e6cd4
--- /dev/null
+++ b/test-suite/output/attributes.v
@@ -0,0 +1,9 @@
+Fail #[canonical=yes, canonical=no] Definition a := 3.
+
+Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3.
+
+Fail #[universes(polymorphic=foo)] Definition a := 3.
+
+Fail #[universes(polymorphic(foo))] Definition a := 3.
+
+Fail #[universes(polymorphic(foo,bar))] Definition a := 3.
diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out
new file mode 100644
index 0000000000..4bc5aafbca
--- /dev/null
+++ b/test-suite/output/bug_10824.out
@@ -0,0 +1,4 @@
+!!
+     : Prop
+!!
+     : Prop
diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v
new file mode 100644
index 0000000000..01271f7d61
--- /dev/null
+++ b/test-suite/output/bug_10824.v
@@ -0,0 +1,12 @@
+Module A.
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End A.
+
+Module B.
+Notation "!!" := False (at level 100).
+Notation F := False.
+Notation "!!" := False (at level 100).
+Check False.
+End B.
diff --git a/test-suite/output/bug_7443.out b/test-suite/output/bug_7443.out
new file mode 100644
index 0000000000..446ec6a1ad
--- /dev/null
+++ b/test-suite/output/bug_7443.out
@@ -0,0 +1,13 @@
+Literal 1
+     : Type
+[1]
+     : Type
+Literal 1
+     : Type
+[1]
+     : Type
+The command has indeed failed with message:
+The term "1" has type "Datatypes.nat" while it is expected to have type
+ "denote ?t".
+Literal 1
+     : Type
diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v
new file mode 100644
index 0000000000..33f76dbcfa
--- /dev/null
+++ b/test-suite/output/bug_7443.v
@@ -0,0 +1,37 @@
+Inductive type := nat | bool.
+Definition denote (t : type)
+  := match t with
+     | nat => Datatypes.nat
+     | bool => Datatypes.bool
+     end.
+Ltac reify t :=
+  lazymatch eval cbv beta in t with
+  | Datatypes.nat => nat
+  | Datatypes.bool => bool
+  end.
+Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
+Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
+Axiom Literal : forall {t}, denote t -> Type.
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Open Scope foo_scope.
+Section A.
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Literal 1 : Type *) (* as expected *)
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable:
+  #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *)
+End A.
+Section B.
+  Notation "[ x ]" := (Literal x) : foo_scope.
+  Check @Literal nat 1. (* [1] : Type *)
+  Fail Check [1]. (* As expected: The command has indeed failed with message:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+   "denote ?t". *)
+  Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope.
+  Check [1]. (* Should succeed, but instead fails with: Error:
+  The term "1" has type "Datatypes.nat" while it is expected to have type
+  "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *)
+End B.
diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out
new file mode 100644
index 0000000000..2d474e4933
--- /dev/null
+++ b/test-suite/output/bug_9569.out
@@ -0,0 +1,16 @@
+1 subgoal
+  
+  ============================
+  exists I : True, I = Logic.I
+1 subgoal
+  
+  ============================
+  f True False True False (Logic.True /\ Logic.False)
+1 subgoal
+  
+  ============================
+  [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I]
+1 subgoal
+  
+  ============================
+  [I & I = Logic.I | I = Logic.I; Logic.I = I]
diff --git a/test-suite/output/bug_9569.v b/test-suite/output/bug_9569.v
new file mode 100644
index 0000000000..ee5b052811
--- /dev/null
+++ b/test-suite/output/bug_9569.v
@@ -0,0 +1,18 @@
+Goal exists I, I = Logic.I.
+Show.
+Abort.
+
+Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r).
+Goal f True False True False (Logic.True /\ Logic.False).
+Show.
+Abort.
+
+Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)).
+Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ].
+Show.
+Abort.
+
+Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..).
+Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ].
+Show.
+Abort.