Revert #8187

8 files changed, 25 insertions, 193 deletions

diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 2ba02924c9..af202ea01c 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,6 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)".
+ "A -> list' A -> list' (A * A)%type".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 For foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index bec4fc1579..94b86fc222 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -72,7 +72,7 @@ Nil
      : forall A : Type, list A
 NIL : list nat
      : list nat
-(false && I 3)%bool /\ (I 6)%bool
+(false && I 3)%bool /\ I 6
      : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 2ffc3b14e2..adab324cf0 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)).
 
 Section A.
 
-Notation "! A" := (forall _:nat, A) (at level 60) : type_scope.
+Notation "! A" := (forall _:nat, A) (at level 60).
 
 Check ! (0=0).
 Check forall n, n=0.
@@ -195,9 +195,9 @@ Open Scope nat_scope.
 
 Coercion is_true := fun b => b=true.
 Coercion of_nat n := match n with 0 => true | _ => false end.
-Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope.
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
 
-Check (false && I 3)%bool /\ (I 6)%bool.
+Check (false && I 3)%bool /\ I 6.
 
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 923caedace..bcb2468792 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -71,7 +71,6 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
 (* Note: does not work for pattern *)
 Module A.
 Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
-Open Scope nat_scope.
 Check fun f x => f x + S x.
 
 Open Scope list_scope.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 015dac2512..d32cf67e28 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -128,27 +128,25 @@ return (1, 2, 3, 4)
      : nat
 *(1.2)
      : nat
-! '{{x, y}}, x + y = 0
+! '{{x, y}}, x.y = 0
      : Prop
 exists x : nat,
   nat ->
   exists y : nat,
-    nat ->
-    exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0
+    nat -> exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x.y = 0 /\ u.t = 0
      : Prop
 exists x : nat,
   nat ->
   exists y : nat,
-    nat ->
-    exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0
+    nat -> exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x.y = 0 /\ z.t = 0
      : Prop
-exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0
+exists_true '{{x, y}} (u := 0) '{{z, t}}, x.y = 0 /\ z.t = 0
      : Prop
 exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R),
 (forall x : A, R x x)
      : Prop
 exists_true (x : nat) (A : Type) (R : A -> A -> Prop) 
-(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z
+(_ : Reflexive R) (y : nat), x.y = 0 -> forall z : A, R z z
      : Prop
 {{{{True, nat -> True}}, nat -> True}}
      : Prop * Prop * Prop
@@ -184,22 +182,22 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
-{'{{x, y}} : nat * nat | x + y = 0}
+{'{{x, y}} : nat * nat | x.y = 0}
      : Set
 exists2' {{x, y}}, x = 0 & y = 0
      : Prop
 myexists2 x : nat * nat,
   let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y
      : Prop
-fun '({{x, y}} as z) => x + y = 0 /\ z = z
+fun '({{x, y}} as z) => x.y = 0 /\ z = z
      : nat * nat -> Prop
-myexists ({{x, y}} as z), x + y = 0 /\ z = z
+myexists ({{x, y}} as z), x.y = 0 /\ z = z
      : Prop
-exists '({{x, y}} as z), x + y = 0 /\ z = z
+exists '({{x, y}} as z), x.y = 0 /\ z = z
      : Prop
-∀ '({{x, y}} as z), x + y = 0 /\ z = z
+∀ '({{x, y}} as z), x.y = 0 /\ z = z
      : Prop
-fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y
+fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y
      : nat * nat * bool -> nat
 myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y
      : Prop
@@ -211,17 +209,17 @@ fun p : nat => if p is S n then n else 0
      : nat -> nat
 fun p : comparison => if p is Lt then 1 else 0
      : comparison -> nat
-fun S : nat => [S | S + S]
+fun S : nat => [S | S.S]
      : nat -> nat * (nat -> nat)
-fun N : nat => [N | N + 0]
+fun N : nat => [N | N.0]
      : nat -> nat * (nat -> nat)
-fun S : nat => [[S | S + S]]
+fun S : nat => [[S | S.S]]
      : nat -> nat * (nat -> nat)
 {I : nat | I = I}
      : Set
 {'I : True | I = I}
      : Prop
-{'{{x, y}} : nat * nat | x + y = 0}
+{'{{x, y}} : nat * nat | x.y = 0}
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
@@ -254,13 +252,3 @@ myfoo01 tt
      : nat
 myfoo01 tt
      : nat
-[{0; 0}]
-     : list (list nat)
-[{1; 2; 3};
- {4; 5; 6};
- {7; 8; 9}]
-     : list (list nat)
-amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
-     : unit
-alist = [0; 1; 2]
-     : list nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 2caffad1d9..dcc8bd7165 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f.
 (* Notations with variables bound both as a term and as a binder      *)
 (* This is #4592 *)
 
-Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope.
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)).
 Check forall n:nat, {# n | 1 > n}.
 
 Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
@@ -183,13 +183,9 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 
 (* Test spacing in #5569 *)
 
-Section S1.
-Variable plus : nat -> nat -> nat.
-Infix "+" := plus.
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
-End S1.
 
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
@@ -197,12 +193,10 @@ Check !!! (x y:nat), True.
 
 (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *)
 
-Section S2.
-Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope.
-Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope.
+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)).
-End S2.
 
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)
@@ -416,58 +410,3 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]
 Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI]  *)
 
 End Issue8126.
-
-(* Test printing of notations guided by scope *)
-
-Module A.
-
-Declare Scope line_scope.
-Delimit Scope line_scope with line.
-Declare Scope matx_scope.
-Notation "{ }" := nil (format "{ }") : line_scope.
-Notation "{ x }" := (cons x nil) : line_scope.
-Notation "{ x ; y ; .. ; z }" :=  (cons x (cons y .. (cons z nil) ..)) : line_scope.
-Notation "[ ]" := nil (format "[ ]") : matx_scope.
-Notation "[ l ]" := (cons l%line nil) : matx_scope.
-Notation "[ l ; l' ; .. ; l'' ]" :=  (cons l%line (cons l'%line .. (cons l''%line nil) ..))
-  (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope.
-
-Open Scope matx_scope.
-Check [[0;0]].
-Check [[1;2;3];[4;5;6];[7;8;9]].
-
-End A.
-
-(* Example by Beta Ziliani *)
-
-Require Import Lists.List.
-
-Module B.
-
-Import ListNotations.
-
-Declare Scope pattern_scope.
-Delimit Scope pattern_scope with pattern.
-
-Declare Scope patterns_scope.
-Delimit Scope patterns_scope with patterns.
-
-Notation "a => b" := (a, b) (at level 201) : pattern_scope.
-Notation "'with' p1 | .. | pn 'end'" :=
-  ((cons p1%pattern (.. (cons pn%pattern nil) ..)))
-    (at level 91, p1 at level 210, pn at level 210) : patterns_scope.
-
-Definition mymatch (n:nat) (l : list (nat * nat)) := tt.
-Arguments mymatch _ _%patterns.
-Notation "'mmatch' n ls" := (mymatch n ls) (at level 0).
-
-Close Scope patterns_scope.
-Close Scope pattern_scope.
-
-Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end.
-Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *)
-
-Definition alist := [0;1;2].
-Print alist.
-
-End B.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index ca20575f1a..9d972a68f7 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -21,30 +21,6 @@ Let "x" e1 e2
      : expr
 Let "x" e1 e2
      : expr
-fun x : nat => (# x)%nat
-     : nat -> nat
-fun x : nat => ## x
-     : nat -> nat
-fun x : nat => # x
-     : nat -> nat
-fun x : nat => ### x
-     : nat -> nat
-fun x : nat => ## x
-     : nat -> nat
-fun x : nat => (x.-1)%pred
-     : nat -> nat
-∀ a : nat, a = 0
-     : Prop
-((∀ a : nat, a = 0) -> True)%type
-     : Prop
-#
-     : Prop
-# -> True
-     : Prop
-((∀ a : nat, a = 0) -> True)%type
-     : Prop
-##
-     : Prop
 myAnd1 True True
      : Prop
 r 2 3
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 3311549013..81c64418cb 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -5,8 +5,8 @@ Module A.
 Declare Custom Entry myconstr.
 
 Notation "[ x ]" := x (x custom myconstr at level 6).
-Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope.
-Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope.
+Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
+Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
 
@@ -95,76 +95,6 @@ Check (Let "x" e1 e2).
 
 End D.
 
-(* Check fix of #8551: a delimiter should be inserted because the
-   lonely notation hides the scope nat_scope, even though the latter
-   is open *)
-
-Module E.
-
-Notation "# x" := (S x) (at level 20) : nat_scope.
-Notation "# x" := (Some x).
-Check fun x => (# x)%nat.
-
-End E.
-
-(* Other tests of precedence *)
-
-Module F.
-
-Notation "# x" := (S x) (at level 20) : nat_scope.
-Notation "## x" := (S x) (at level 20).
-Check fun x => S x.
-Open Scope nat_scope.
-Check fun x => S x.
-Notation "### x" := (S x) (at level 20) : nat_scope.
-Check fun x => S x.
-Close Scope nat_scope.
-Check fun x => S x.
-
-End F.
-
-(* Lower priority of generic application rules *)
-
-Module G.
-
-Declare Scope predecessor_scope.
-Delimit Scope predecessor_scope with pred.
-Declare Scope app_scope.
-Delimit Scope app_scope with app.
-Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope.
-Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope.
-Check fun x => pred x.
-
-End G.
-
-(* Checking arbitration between in the presence of a notation in type scope *)
-
-Module H.
-
-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 a, a = 0.
-
-Close Scope type_scope.
-Check ((forall a, a = 0) -> True)%type.
-Open Scope type_scope.
-
-Notation "#" := (forall a, a = 0).
-Check #.
-Check # -> True.
-
-Close Scope type_scope.
-Check (# -> True)%type.
-Open Scope type_scope.
-
-Declare Scope my_scope.
-Notation "##" := (forall a, a = 0) : my_scope.
-Open Scope my_scope.
-Check ##.
-
-End H.
-
 (* Fixing bugs reported by G. Gonthier in #9207 *)
 
 Module I.