Revert "Merge PR #873: New strategy based on open scopes for deciding which notation to use among several of them"

This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.

6 files changed, 26 insertions, 95 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 891296b0a..b60b1ee86 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -64,7 +64,7 @@ The command has indeed failed with message:
 Cannot find where the recursive pattern starts.
 The command has indeed failed with message:
 Both ends of the recursive pattern are the same.
-(nat * nat + nat)%type
+SUM (nat * nat) nat
      : Set
 FST (0; 1)
      : Z
@@ -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 413812ee1..fe6c05c39 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.
@@ -194,9 +194,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.out b/test-suite/output/Notations2.out
index 6ffe56e11..41d159375 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -37,13 +37,13 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : (nat -> nat) -> nat -> nat
 Notation plus2 n := (S(S(n)))
 λ n : list(nat), match n with
-                 | 1 :: nil => 0
+                 | list1 => 0
                  | _ => 2
                  end
      : list(nat) -> nat
 λ n : list(nat),
 match n with
-| 1 :: nil => 0
+| list1 => 0
 | nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2
 end
      : list(nat) -> nat
@@ -51,7 +51,7 @@ end
 match n with
 | nil => 2
 | 0 :: _ => 2
-| 1 :: nil => 0
+| list1 => 0
 | 1 :: _ :: _ => 2
 | plus2 _ :: _ => 2
 end
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 923caedac..bcb246879 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 864b6151a..1987b6a6e 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -128,37 +128,25 @@ return (1, 2, 3, 4)
      : nat
 *(1.2)
      : 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
-! '{{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
@@ -194,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
@@ -221,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
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index c98bfff41..c165f9553 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,62 +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 printing of notations guided by scope *)
-
-Module A.
-
-Delimit Scope line_scope with line.
-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.
-
-Delimit Scope pattern_scope with pattern.
-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.
 
 (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *)
 (* for isolated "forall" (was not working already in 8.6) *)