9 files changed, 207 insertions, 20 deletions
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 5f22eb5d7c..ef7667936c 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -1,4 +1,4 @@
-compose (C:=nat) S
+compose S
      : (nat -> nat) -> nat -> nat
 ex_intro (P:=fun _ : nat => True) (x:=0) I
      : ex (fun _ : nat => True)
@@ -12,3 +12,8 @@ map id' (1 :: nil)
      : list nat
 map (id'' (A:=nat)) (1 :: nil)
      : list nat
+fix f (x : nat) : option nat := match x with
+                                | 0 => None
+                                | S _ => x
+                                end
+     : nat -> option nat
diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v
index 306532c0df..a7c4399e38 100644
--- a/test-suite/output/Implicit.v
+++ b/test-suite/output/Implicit.v
@@ -51,3 +51,13 @@ Definition id'' (A:Type) (x:A) := x.
 
 Check map (@id'' nat) (1::nil).
 
+Module MatchBranchesInContext.
+
+Set Implicit Arguments.
+Set Contextual Implicit.
+
+Inductive option A := None | Some (a:A).
+Coercion some_nat := @Some nat.
+Check fix f x := match x with 0 => None | n => some_nat n end.
+
+End MatchBranchesInContext.
diff --git a/test-suite/output/ImplicitTypes.out b/test-suite/output/ImplicitTypes.out
new file mode 100644
index 0000000000..824c260e92
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.out
@@ -0,0 +1,26 @@
+forall b, b = b
+     : Prop
+forall b : nat, b = b
+     : Prop
+forall b : bool, @eq bool b b
+     : Prop
+forall b : bool, b = b
+     : Prop
+forall b c : bool, b = c
+     : Prop
+forall c b : bool, b = c
+     : Prop
+forall b1 b2, b1 = b2
+     : Prop
+fun b => b = b
+     : bool -> Prop
+fix f b (n : nat) {struct n} : bool :=
+  match n with
+  | 0 => b
+  | S p => f b p
+  end
+     : bool -> nat -> bool
+∀ b c : bool, b = c
+     : Prop
+∀ b1 b2, b1 = b2
+     : Prop
diff --git a/test-suite/output/ImplicitTypes.v b/test-suite/output/ImplicitTypes.v
new file mode 100644
index 0000000000..dbc83f9229
--- /dev/null
+++ b/test-suite/output/ImplicitTypes.v
@@ -0,0 +1,37 @@
+Implicit Types b : bool.
+Check forall b, b = b.
+
+(* Check the type is not used if not the reserved one *)
+Check forall b:nat, b = b.
+
+(* Check full printing *)
+Set Printing All.
+Check forall b, b = b.
+Unset Printing All.
+
+(* Check printing of type *)
+Unset Printing Use Implicit Types.
+Check forall b, b = b.
+Set Printing Use Implicit Types.
+
+(* Check factorization: we give priority on factorization over implicit type *)
+Check forall b c, b = c.
+Check forall c b, b = c.
+
+(* Check factorization of implicit types *)
+Check forall b1 b2, b1 = b2.
+
+(* Check in "fun" *)
+Check fun b => b = b.
+
+(* Check in binders *)
+Check fix f b n := match n with 0 => b | S p => f b p end.
+
+(* Check in notations *)
+Module Notation.
+  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 b c, b = c.
+  Check forall b1 b2, b1 = b2.
+End Notation.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 1c8f237bb8..e121b5e86c 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,8 +14,6 @@ Entry constr:myconstr is
      : nat
 [<< # 0 >>]
      : option nat
-[2 + 3]
-     : nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
@@ -77,3 +75,35 @@ Entry constr:expr is
 [ "201" RIGHTA
   [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
 
+fun x : nat => [ x ]
+     : nat -> nat
+fun x : nat => [x]
+     : nat -> nat
+∀ x : nat, x = x
+     : Prop
+File "stdin", line 219, characters 0-160:
+Warning: Notation "∀ _ .. _ , _" was already defined with a different format
+in scope type_scope. [notation-incompatible-format,parsing]
+∀x : nat,x = x
+     : Prop
+File "stdin", line 232, characters 0-60:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 236, characters 0-64:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 241, characters 0-62:
+Warning: Lonely notation "_ %%%% _" was already defined with a different
+format. [notation-incompatible-format,parsing]
+3  %%  4
+     : nat
+3  %%  4
+     : nat
+3   %%   4
+     : nat
+File "stdin", line 269, characters 0-61:
+Warning: The format modifier is irrelevant for only parsing rules.
+[irrelevant-format-only-parsing,parsing]
+File "stdin", line 273, characters 0-63:
+Warning: The only parsing modifier has no effect in Reserved Notation.
+[irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..1cf0d919b1 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,9 +22,6 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
 Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
 Check [ << # 0 >> ].
 
-Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
-Check [ 2 + 3 ].
-
 End A.
 
 Module B.
@@ -195,3 +192,84 @@ Notation "{ p }" := (p) (in custom expr at level 201, p constr).
 Print Custom Grammar expr.
 
 End Bug11331.
+
+Module Bug_6082.
+
+Declare Scope foo.
+Notation "[ x ]" := (S x) (format "[  x  ]") : foo.
+Open Scope foo.
+Check fun x => S x.
+
+Declare Scope bar.
+Notation "[ x ]" := (S x) (format "[ x ]") : bar.
+Open Scope bar.
+
+Check fun x => S x.
+
+End Bug_6082.
+
+Module Bug_7766.
+
+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 : nat), x = x.
+
+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 : nat), x = x.
+
+End Bug_7766.
+
+Module N.
+
+(* Other tests about generic and specific formats *)
+
+Reserved Notation "x %%% y" (format "x  %%%  y", at level 35).
+Reserved Notation "x %%% y" (format "x %%% y", at level 35).
+
+(* Not using the reserved format, we warn *)
+
+Notation "x %%% y" := (x+y) (format "x   %%%   y", at level 35).
+
+(* Same scope (here lonely): we warn *)
+
+Notation "x %%%% y" := (x+y) (format "x  %%%%  y", at level 35).
+Notation "x %%%% y" := (x+y) (format "x %%%% y", at level 35).
+
+(* Test if the format for a specific notation becomes the default
+   generic format or if the generic format, in the absence of a
+   Reserved Notation, is the one canonically obtained from the
+   notation *)
+
+Declare Scope foo_scope.
+Declare Scope bar_scope.
+Declare Scope bar'_scope.
+Notation "x %% y" := (x+y) (at level 47, format "x   %%   y") : foo_scope.
+Open Scope foo_scope.
+Check 3 %% 4.
+
+(* No scope, we inherit the initial format *)
+
+Notation "x %% y" := (x*y) : bar_scope. (* Inherit the format *)
+Open Scope bar_scope.
+Check 3 %% 4.
+
+(* Different scope and no reserved notation, we don't warn *)
+
+Notation "x %% y" := (x*y) (at level 47, format "x    %%    y") : bar'_scope.
+Open Scope bar'_scope.
+Check 3 %% 4.
+
+(* Warn for combination of "only parsing" and "format" *)
+
+Notation "###" := 0 (at level 0, only parsing, format "###").
+
+(* In reserved notation, warn only for the "only parsing" *)
+
+Reserved Notation "##" (at level 0, only parsing, format "##").
+
+End N.
diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 83dd2f40fb..c5b4d6f291 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -6,13 +6,13 @@ where
 ?B : [ |- Type]
 p 0
      : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
-p 0 0 (B:=bool)
+p 0 0
      : forall b : bool, 0 = 0 /\ b = b
-p 0 0 (B:=bool)
+p 0 0
      : forall b : bool, 0 = 0 /\ b = b
-p (A:=nat)
+p
      : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
-p (A:=nat)
+p
      : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
 @p nat 0 0
      : forall (B : Type) (b : B), 0 = 0 /\ b = b
@@ -44,16 +44,16 @@ p
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 f x true
      : 0 = 0 /\ true = true
-f x (B:=bool)
+f x
      : forall b : bool, 0 = 0 /\ b = b
-f x (B:=bool)
+f x
      : forall b : bool, 0 = 0 /\ b = b
 @f nat
      : forall a1 a2 : nat,
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
 @f
      : forall (A : Type) (a1 a2 : A),
@@ -62,16 +62,16 @@ f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
 x.(f) true
      : 0 = 0 /\ true = true
-x.(f) (B:=bool)
+x.(f)
      : forall b : bool, 0 = 0 /\ b = b
-x.(f) (B:=bool)
+x.(f)
      : forall b : bool, 0 = 0 /\ b = b
 @f nat
      : forall a1 a2 : nat,
        T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
-f (a1:=0) (a2:=0)
+f
      : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
 @f
      : forall (A : Type) (a1 a2 : A),
@@ -218,7 +218,7 @@ p 0 0
      : forall b : ?B, 0 = 0 /\ b = b
 where
 ?B : [ |- Type]
-p 0 0 (B:=bool)
+p 0 0
      : forall b : bool, 0 = 0 /\ b = b
 p 0 0 true
      : 0 = 0 /\ true = true
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 505dc52ebe..113384e9cf 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -75,7 +75,7 @@ The command has indeed failed with message:
 In environment
 v := 0 : nat
 The term "v" has type "nat" while it is expected to have type "wuint".
-File "stdin", line 202, characters 2-72:
+File "stdin", line 203, characters 2-72:
 Warning: The 'abstract after' directive has no effect when the parsing
 function (of_uint) targets an option type.
 [abstract-large-number-no-op,numbers]
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index c306b15ef3..22aff36d67 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -123,6 +123,7 @@ Module Test6.
     Export Scopes.
     Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000).
   End Notations.
+  Set Printing Coercions.
   Check let v := 0%wnat in v : wnat.
   Check wrap O.
   Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *)