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.

10 files changed, 41 insertions, 137 deletions

diff --git a/CHANGES b/CHANGES
index 320b325ae..1ed110b4b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,10 +7,6 @@ Notations
   right (e.g. "( x ; .. ; y ; z )") now supported.
 - Notations with a specific level for the leftmost nonterminal,
   when printing-only, are supported.
-- When several notations are available for the same expression,
-  priority is given to latest notations defined in the scopes being
-  opened rather than to the latest notations defined independently of
-  whether they are in an opened scope or not.
 - Notations can now refer to the syntactic category of patterns (as in
   "fun 'pat =>" or "match p with pat => ... end"). Two variants are
   available, depending on whether a single variable is considered as a
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 949c7cbd8..9efaff3b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -386,7 +386,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
     try
       if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_pattern scopes vars pat
-        (uninterp_cases_pattern_notations scopes pat)
+        (uninterp_cases_pattern_notations pat)
     with No_match ->
       lift (fun ?loc -> function
 	| PatVar (Name id) -> CPatAtom (Some (Ident (loc,id)))
@@ -517,7 +517,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
 	extern_notation_ind_pattern scopes vars ind args
-          (uninterp_ind_pattern_notations scopes ind)
+          (uninterp_ind_pattern_notations ind)
     with No_match ->
       let c = extern_reference vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
@@ -741,7 +741,7 @@ let rec extern inctx scopes vars r =
   try
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_notation scopes vars r'' (uninterp_notations scopes r'')
+    extern_notation scopes vars r'' (uninterp_notations r'')
   with No_match -> lift (fun ?loc -> function
   | GRef (ref,us) ->
       extern_global (select_stronger_impargs (implicits_of_global ref))
diff --git a/interp/notation.ml b/interp/notation.ml
index da3ed6b8c..47d648135 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -545,38 +545,15 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
-let sort_notations scopes l =
-  let extract_scope l = function
-    | Scope sc -> List.partitioni (fun _i x ->
-                      match x with
-                      | NotationRule (Some sc',_),_,_ -> String.equal sc sc'
-                      | _ -> false) l
-    | SingleNotation ntn -> List.partitioni (fun _i x ->
-                      match x with
-                      | NotationRule (None,ntn'),_,_ -> String.equal ntn ntn'
-                      | _ -> false) l in
-  let rec aux l scopes =
-    if l == [] then [] (* shortcut *) else
-    match scopes with
-    | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes
-    | [] -> l in
-  aux l scopes
-
-let uninterp_notations scopes c =
-  let scopes = make_current_scopes scopes in
-  let keys = glob_constr_keys c in
-  let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in
-  sort_notations scopes maps
-
-let uninterp_cases_pattern_notations scopes c =
-  let scopes = make_current_scopes scopes in
-  let maps = keymap_find (cases_pattern_key c) !notations_key_table in
-  sort_notations scopes maps
-
-let uninterp_ind_pattern_notations scopes ind =
-  let scopes = make_current_scopes scopes in
-  let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in
-  sort_notations scopes maps
+let uninterp_notations c =
+  List.map_append (fun key -> keymap_find key !notations_key_table)
+    (glob_constr_keys c)
+
+let uninterp_cases_pattern_notations c =
+  keymap_find (cases_pattern_key c) !notations_key_table
+
+let uninterp_ind_pattern_notations ind =
+  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
diff --git a/interp/notation.mli b/interp/notation.mli
index aa52b858a..6803a7e51 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -126,9 +126,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
 type notation_rule = interp_rule * interpretation * int option
 
 (** Return the possible notations for a given term *)
-val uninterp_notations : local_scopes -> 'a glob_constr_g -> notation_rule list
-val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list
-val uninterp_ind_pattern_notations : local_scopes -> inductive -> notation_rule list
+val uninterp_notations : 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list
+val uninterp_ind_pattern_notations : inductive -> notation_rule list
 
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
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) *)