Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes)

14 files changed, 552 insertions, 171 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 1f88b77b51..7a4af0d7a8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -148,6 +148,11 @@ Notations
   that will do it automatically, using the output of coqc. The script
   contains documentation on its usage in a comment at the top.
 
+- When several notations are available for the same expression,
+  priority is given to latest notations defined in the scopes being
+  opened, in order, rather than to the latest notations defined
+  independently of whether they are in an opened scope or not.
+
 Tactics
 
 - Added toplevel goal selector `!` which expects a single focused goal.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index acb0d80c18..c0f15f02a5 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -152,6 +152,12 @@ Termops
 - Internal printing functions have been placed under the
   `Termops.Internal` namespace.
 
+Notations:
+
+- Notation.availability_of_notation is not anymore needed: if a
+  delimiter is needed, it is provided by Notation.uninterp_notation
+  which fails in case the notation is not available.
+
 ### Unit testing
 
 The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 1c53f5981d..a5869055fa 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1040,6 +1040,8 @@ interpreted in the scope stack extended with the scope bound tokey.
    To remove a delimiting key of a scope, use the command
    :n:`Undelimit Scope @scope`
 
+.. _ArgumentScopes:
+
 Binding arguments of a constant to an interpretation scope
 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
@@ -1307,6 +1309,65 @@ Displaying information about scopes
       It also displays the delimiting key if any and the class to which the
       scope is bound, if any.
 
+Impact of scopes on printing
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When several notations are available for printing the same expression,
+Coq will use the following rules for printing priorities:
+
+- If two notations are available in different scopes which are open,
+  the notation in the more recently opened scope takes precedence.
+
+- If two notations are available in the same scope, the more recently
+  defined (or imported) notation takes precedence.
+
+- Abbreviations and lonely notations, both of which have no scope,
+  take precedence over a notation in an open scope if and only if the
+  abbreviation or lonely notation was defined (or imported) more
+  recently than when the corresponding scope was open. They take
+  precedence over any notation not in an open scope, whether this scope
+  has a delimiter or not.
+
+- A scope is *active* for printing a term either because it was opened
+  with :cmd:`Open Scope`, or the term is the immediate argument of a
+  constant which temporarily opens a scope for this argument (see
+  :ref:`Arguments <ArgumentScopes>`) in which case this temporary
+  scope is the most recent open one.
+
+- In case no abbreviation, nor lonely notation, nor notation in an
+  explicitly open scope, nor notation in a temporarily open scope of
+  arguments, has been found, notations in those closed scopes which
+  have a delimiter are considered, giving priority to the most
+  recently defined (or imported) ones. The corresponding delimiter is
+  inserted, making the corresponding scope the most recent explicitly
+  open scope for all subterms of the current term. As an exception to
+  the insertion of the corresponding delimiter, when an expression is
+  statically known to be in a position expecting a type and the
+  notation is from scope ``type_scope``, and the latter is closed, the
+  delimiter is not inserted. This is because expressions statically
+  known to be in a position expecting a type are by default
+  interpreted with `type_scope` temporarily activated. Expressions
+  statically known to be in a position expecting a type typically
+  include being on the right-hand side of `:`, `<:`, `<<:` and after
+  the comma in a `forall` expression.
+
+- As a refinement of the previous rule, in the case of applied global
+  references, notations in a non-opened scope with delimiter
+  specifically defined for this applied global reference take priority
+  over notations in a non-opened scope with delimiter for generic
+  applications. For instance, in the presence of ``Notation "f ( x
+  )" := (f x) (at level 10, format "f ( x )") : app_scope`` and
+  ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") :
+  mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being
+  bound to a delimiter *and* both not opened, the latter, more
+  specific notation will always take precedence over the first, more
+  generic one.
+
+- A scope can be closed by using :cmd:`Close Scope` and its delimiter
+  removed by using :cmd:`Undelimit Scope`. To remove automatic
+  temporary opening of scopes for arguments of a constant, use
+  :ref:`Arguments <ArgumentScopes>`.
+
 .. _Abbreviations:
 
 Abbreviations
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 25f2526f74..fba03b9de9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -110,13 +110,13 @@ let deactivate_notation nr =
      (* shouldn't we check wether it is well defined? *)
      inactive_notations_table := IRuleSet.add nr !inactive_notations_table
   | NotationRule (scopt, ntn) ->
-     match availability_of_notation (scopt, ntn) (scopt, []) with
-     | None -> user_err ~hdr:"Notation"
+     if not (exists_notation_interpretation_in_scope scopt ntn) then
+       user_err ~hdr:"Notation"
                         (pr_notation ntn ++ spc () ++ str "does not exist"
                          ++ (match scopt with
                              | None -> spc () ++ str "in the empty scope."
                              | Some _ -> show_scope scopt ++ str "."))
-     | Some _ ->
+     else
         if IRuleSet.mem nr !inactive_notations_table then
           Feedback.msg_warning
             (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
@@ -263,6 +263,11 @@ let rec insert_pat_coercion ?loc l c = match l with
   | [] -> c
   | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
 
+let add_lonely keyrule seen =
+  match keyrule with
+  | NotationRule (None,ntn) -> ntn::seen
+  | SynDefRule _ | NotationRule (Some _,_) -> seen
+
 (**********************************************************************)
 (* conversion of references                                           *)
 
@@ -387,8 +392,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   with No_match ->
     try
       if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
-      extern_notation_pattern allscopes vars pat
-        (uninterp_cases_pattern_notations pat)
+      extern_notation_pattern allscopes [] vars pat
+        (uninterp_cases_pattern_notations scopes pat)
     with No_match ->
     let loc = pat.CAst.loc in
     match DAst.get pat with
@@ -441,18 +446,15 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       insert_pat_coercion coercion pat
 
 and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
-    (custom, (tmp_scope, scopes) as allscopes) vars =
+    (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars =
   function
-    | NotationRule (sc,ntn) ->
+    | NotationRule (sc,ntn),key,need_delim ->
       begin
         match availability_of_entry_coercion custom (fst ntn) with
         | None -> raise No_match
         | Some coercion ->
-        match availability_of_notation (sc,ntn) (tmp_scope,scopes) with
-	  (* Uninterpretation is not allowed in current context *)
-	  | None -> raise No_match
-	  (* Uninterpretation is allowed in current context *)
-	  | Some (scopt,key) ->
+            let key = if need_delim || List.mem ntn lonely_seen then key else None in
+            let scopt = match key with Some _ -> sc | _ -> None in
 	    let scopes' = Option.List.cons scopt scopes in
 	    let l =
               List.map (fun (c,(subentry,(scopt,scl))) ->
@@ -474,7 +476,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
               (insert_pat_delimiters ?loc
                  (make_pat_notation ?loc ntn (l,ll) l2') key)
       end
-    | SynDefRule kn ->
+    | SynDefRule kn,key,need_delim ->
+      assert (key = None && need_delim = false);
       match availability_of_entry_coercion custom InConstrEntrySomeLevel with
       | None -> raise No_match
       | Some coercion ->
@@ -492,9 +495,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       in
       assert (List.is_empty substlist);
       insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
-and extern_notation_pattern allscopes vars t = function
+and extern_notation_pattern allscopes lonely_seen vars t = function
   | [] -> raise No_match
-  | (keyrule,pat,n as _rule)::rules ->
+  | (keyrule,pat,n as _rule,key,need_delim)::rules ->
     try
       if is_inactive_rule keyrule then raise No_match;
       let loc = t.loc in
@@ -502,22 +505,27 @@ and extern_notation_pattern allscopes vars t = function
         | PatCstr (cstr,args,na) ->
           let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
 	  let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
-	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
+            (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars
+            (keyrule,key,need_delim) in
 	  insert_pat_alias ?loc p na
 	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
         | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
     with
-	No_match -> extern_notation_pattern allscopes vars t rules
+      No_match ->
+      let lonely_seen = add_lonely keyrule lonely_seen in
+      extern_notation_pattern allscopes lonely_seen vars t rules
 
-let rec extern_notation_ind_pattern allscopes vars ind args = function
+let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function
   | [] -> raise No_match
-  | (keyrule,pat,n as _rule)::rules ->
+  | (keyrule,pat,n as _rule,key,need_delim)::rules ->
     try
       if is_inactive_rule keyrule then raise No_match;
       apply_notation_to_pattern (IndRef ind)
-	(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
+        (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim)
     with
-	No_match -> extern_notation_ind_pattern allscopes vars ind args rules
+      No_match ->
+      let lonely_seen = add_lonely keyrule lonely_seen in
+      extern_notation_ind_pattern allscopes lonely_seen vars ind args rules
 
 let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
@@ -529,8 +537,8 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
-      extern_notation_ind_pattern allscopes vars ind args
-          (uninterp_ind_pattern_notations ind)
+      extern_notation_ind_pattern allscopes [] vars ind args
+          (uninterp_ind_pattern_notations scopes ind)
     with No_match ->
       let c = extern_reference vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
@@ -760,32 +768,32 @@ let extern_ref vars ref us =
 
 let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 
-let rec extern inctx scopes vars r =
+let rec extern inctx (custom,scopes as allscopes) vars r =
   let r' = remove_coercions inctx r in
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_optimal (extern_possible_prim_token scopes) r r'
+    extern_optimal (extern_possible_prim_token allscopes) r r'
   with No_match ->
   try
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_optimal
-      (fun r -> extern_notation scopes vars r (uninterp_notations r))
+      (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r))
       r r''
   with No_match ->
   let loc = r'.CAst.loc in
   match DAst.get r' with
-  | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
+  | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us)
 
-  | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+  | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id)
 
   | c ->
 
-  match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
+  match availability_of_entry_coercion custom InConstrEntrySomeLevel with
   | None -> raise No_match
   | Some coercion ->
 
-  let scopes = (InConstrEntrySomeLevel, snd scopes) in
+  let scopes = (InConstrEntrySomeLevel, scopes) in
   let c = match c with
 
   (* The remaining cases are only for the constr entry *)
@@ -797,7 +805,7 @@ let rec extern inctx scopes vars r =
   | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
 
   | GEvar (n,l) ->
-      extern_evar n (List.map (on_snd (extern false scopes vars)) l)
+      extern_evar n (List.map (on_snd (extern false allscopes vars)) l)
 
   | GPatVar kind ->
       if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
@@ -1056,9 +1064,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
   make ?loc (pll,extern inctx scopes vars c)
 
-and extern_notation (custom,scopes as allscopes) vars t = function
+and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
   | [] -> raise No_match
-  | (keyrule,pat,n as _rule)::rules ->
+  | (keyrule,pat,n as _rule,key,need_delim)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
       try
         if is_inactive_rule keyrule then raise No_match;
@@ -1106,11 +1114,8 @@ and extern_notation (custom,scopes as allscopes) vars t = function
              (match availability_of_entry_coercion custom (fst ntn) with
              | None -> raise No_match
              | Some coercion ->
-               match availability_of_notation (sc,ntn) scopes with
-                  (* Uninterpretation is not allowed in current context *)
-              | None -> raise No_match
-                  (* Uninterpretation is allowed in current context *)
-	      | Some (scopt,key) ->
+                  let key = if need_delim || List.mem ntn lonely_seen then key else None in
+                  let scopt = match key with Some _ -> sc | None -> None in
                   let scopes' = Option.List.cons scopt (snd scopes) in
 	          let l =
                     List.map (fun (c,(subentry,(scopt,scl))) ->
@@ -1146,7 +1151,9 @@ and extern_notation (custom,scopes as allscopes) vars t = function
 	  let args = extern_args (extern true) vars args in
 	  CAst.make ?loc @@ explicitize false argsimpls (None,e) args
       with
-	  No_match -> extern_notation allscopes vars t rules
+        No_match ->
+        let lonely_seen = add_lonely keyrule lonely_seen in
+        extern_notation allscopes lonely_seen vars t rules
 
 and extern_recursion_order scopes vars = function
     GStructRec -> CStructRec
diff --git a/interp/notation.ml b/interp/notation.ml
index db8ee5bc18..0af75b5bfa 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -21,6 +21,7 @@ open Notation_term
 open Glob_term
 open Glob_ops
 open Context.Named.Declaration
+open Classops
 
 (*i*)
 
@@ -156,6 +157,8 @@ let scope_eq s1 s2 = match s1, s2 with
 | Scope _, SingleNotation _
 | SingleNotation _, Scope _ -> false
 
+(* Scopes for interpretation *)
+
 let scope_stack = ref []
 
 let current_scopes () = !scope_stack
@@ -165,14 +168,91 @@ let scope_is_open_in_scopes sc l =
 
 let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 
+(* Uninterpretation tables *)
+
+type interp_rule =
+  | NotationRule of scope_name option * notation
+  | SynDefRule of KerName.t
+
+type scoped_notation_rule_core = scope_name * notation * interpretation * int option
+type notation_rule_core = interp_rule * interpretation * int option
+type notation_rule = notation_rule_core * delimiters option * bool
+
+(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and  *)
+
+type uninterp_scope_elem =
+  | UninterpScope of scope_name
+  | UninterpSingle of notation_rule_core
+
+let uninterp_scope_eq_weak s1 s2 = match s1, s2 with
+| UninterpScope s1, UninterpScope s2 -> String.equal s1 s2
+| UninterpSingle s1, UninterpSingle s2 -> false
+| (UninterpSingle _ | UninterpScope _), _ -> false
+
+module ScopeOrd =
+  struct
+    type t = scope_name option
+    let compare = Pervasives.compare
+  end
+
+module ScopeMap = CMap.Make(ScopeOrd)
+
+let uninterp_scope_stack = ref []
+
+let push_uninterp_scope sc scopes = UninterpScope sc :: scopes
+
+let push_uninterp_scopes = List.fold_right push_uninterp_scope
+
+(**********************************************************************)
+(* Mapping classes to scopes *)
+
+type scope_class = cl_typ
+
+let scope_class_compare : scope_class -> scope_class -> int =
+  cl_typ_ord
+
+let compute_scope_class sigma t =
+  let (cl,_,_) = find_class_type sigma t in
+  cl
+
+module ScopeClassOrd =
+struct
+  type t = scope_class
+  let compare = scope_class_compare
+end
+
+module ScopeClassMap = Map.Make(ScopeClassOrd)
+
+let initial_scope_class_map : scope_name ScopeClassMap.t =
+  ScopeClassMap.empty
+
+let scope_class_map = ref initial_scope_class_map
+
+let declare_scope_class sc cl =
+  scope_class_map := ScopeClassMap.add cl sc !scope_class_map
+
+let find_scope_class cl =
+  ScopeClassMap.find cl !scope_class_map
+
+let find_scope_class_opt = function
+  | None -> None
+  | Some cl -> try Some (find_scope_class cl) with Not_found -> None
+
+let current_type_scope_name () =
+   find_scope_class_opt (Some CL_SORT)
+
 (* TODO: push nat_scope, z_scope, ... in scopes summary *)
 
 (* Exportation of scopes *)
 let open_scope i (_,(local,op,sc)) =
-  if Int.equal i 1 then
+  if Int.equal i 1 then begin
     scope_stack :=
-      if op then sc :: !scope_stack
-      else List.except scope_eq sc !scope_stack
+      if op then Scope sc :: !scope_stack
+      else List.except scope_eq (Scope sc) !scope_stack;
+    uninterp_scope_stack :=
+      if op then UninterpScope sc :: !uninterp_scope_stack
+      else List.except uninterp_scope_eq_weak (UninterpScope sc) !uninterp_scope_stack
+    end
 
 let cache_scope o =
   open_scope 1 o
@@ -187,7 +267,7 @@ let discharge_scope (_,(local,_,_ as o)) =
 let classify_scope (local,_,_ as o) =
   if local then Dispose else Substitute o
 
-let inScope : bool * bool * scope_elem -> obj =
+let inScope : bool * bool * scope_name -> obj =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
@@ -196,7 +276,7 @@ let inScope : bool * bool * scope_elem -> obj =
       classify_function = classify_scope }
 
 let open_close_scope (local,opening,sc) =
-  Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc)))
+  Lib.add_anonymous_leaf (inScope (local,opening,normalize_scope sc))
 
 let empty_scope_stack = []
 
@@ -204,9 +284,20 @@ let push_scope sc scopes = Scope sc :: scopes
 
 let push_scopes = List.fold_right push_scope
 
+let make_type_scope_soft tmp_scope =
+  if Option.equal String.equal tmp_scope (current_type_scope_name ()) then
+    true, None
+  else
+    false, tmp_scope
+
 let make_current_scopes (tmp_scope,scopes) =
   Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
 
+let make_current_uninterp_scopes (tmp_scope,scopes) =
+  let istyp,tmp_scope = make_type_scope_soft tmp_scope in
+  istyp,Option.fold_right push_uninterp_scope tmp_scope
+    (push_uninterp_scopes scopes !uninterp_scope_stack)
+
 (**********************************************************************)
 (* Delimiters *)
 
@@ -250,40 +341,80 @@ let find_delimiters_scope ?loc key =
     user_err ?loc ~hdr:"find_delimiters"
       (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
-(* Uninterpretation tables *)
-
-type interp_rule =
-  | NotationRule of scope_name option * notation
-  | SynDefRule of KerName.t
-
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
 type key =
   | RefKey of GlobRef.t
+  | LambdaKey
+  | ProdKey
   | Oth
 
 let key_compare k1 k2 = match k1, k2 with
 | RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
-| RefKey _, Oth -> -1
-| Oth, RefKey _ -> 1
-| Oth, Oth -> 0
+| RefKey _, _ -> -1
+| _, RefKey _ -> 1
+| k1, k2 -> Pervasives.compare k1 k2
 
 module KeyOrd = struct type t = key let compare = key_compare end
 module KeyMap = Map.Make(KeyOrd)
 
-type notation_rule = interp_rule * interpretation * int option
-
-let keymap_add key interp map =
-  let old = try KeyMap.find key map with Not_found -> [] in
-  KeyMap.add key (interp :: old) map
+let keymap_add key sc interp (scope_map,global_map) =
+  (* Adding to scope keymap for printing based on open scopes *)
+  let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in
+  let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in
+  let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in
+  let scope_map = ScopeMap.add sc newscmap scope_map in
+  (* Adding to global keymap of scoped notations in case the scope is not open *)
+  let global_map = match interp with
+  | NotationRule (Some sc,ntn), interp, c ->
+      let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in
+      KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map
+  | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in
+  (scope_map, global_map)
+
+let keymap_extract istype keys sc map =
+  let keymap =
+    try ScopeMap.find (Some sc) map
+    with Not_found -> KeyMap.empty in
+  let delim =
+    if istype && Option.equal String.equal (Some sc) (current_type_scope_name ()) then
+      (* A type is re-interpreted with type_scope on top, so never need a delimiter *)
+      None
+    else
+      (* Pass the delimiter so that it can be used if ever the notation is masked *)
+      (String.Map.find sc !scope_map).delimiters in
+  let add_scope rule = (rule,delim,false) in
+  List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys
+
+let find_with_delimiters istype = function
+  | None ->
+      None
+  | Some _ as scope when istype && Option.equal String.equal scope (current_type_scope_name ()) ->
+      (* This is in case type_scope (which by default is open in the
+         initial state) has been explicitly closed *)
+      Some None
+  | Some scope ->
+      match (String.Map.find scope !scope_map).delimiters with
+        | Some key -> Some (Some key)
+        | None -> None
 
-let keymap_find key map =
-  try KeyMap.find key map
-  with Not_found -> []
+let rec keymap_extract_remainder istype scope_seen = function
+  | [] -> []
+  | (sc,ntn,interp,c) :: l ->
+      if String.Set.mem sc scope_seen then keymap_extract_remainder istype scope_seen l
+      else
+        match find_with_delimiters istype (Some sc) with
+        | None -> keymap_extract_remainder istype scope_seen l
+        | Some delim ->
+           let rule = (NotationRule (Some sc, ntn), interp, c) in
+           (rule,delim,true) :: keymap_extract_remainder istype scope_seen l
 
 (* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
+let notations_key_table =
+  ref ((ScopeMap.empty, KeyMap.empty) :
+       notation_rule_core list KeyMap.t ScopeMap.t *
+       scoped_notation_rule_core list KeyMap.t)
 
 let glob_prim_constr_key c = match DAst.get c with
   | GRef (ref, _) -> Some (canonical_gr ref)
@@ -295,12 +426,14 @@ let glob_prim_constr_key c = match DAst.get c with
   | _ -> None
 
 let glob_constr_keys c = match DAst.get c with
+  | GRef (ref,_) -> [RefKey (canonical_gr ref)]
   | GApp (c, _) ->
     begin match DAst.get c with
     | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth]
     | _ -> [Oth]
     end
-  | GRef (ref,_) -> [RefKey (canonical_gr ref)]
+  | GLambda _ -> [LambdaKey]
+  | GProd _ -> [ProdKey]
   | _ -> [Oth]
 
 let cases_pattern_key c = match DAst.get c with
@@ -314,6 +447,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
       RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | NApp (_,args) -> Oth, Some (List.length args)
+  | NLambda _ | NBinderList (_,_,NLambda _,_,_) | NList (_,_,NLambda _,_,_) -> LambdaKey, None
+  | NProd _ | NBinderList (_,_,NProd _,_,_) | NList (_,_,NProd _,_,_) -> ProdKey, None
   | _ -> Oth, None
 
 (**********************************************************************)
@@ -839,37 +974,31 @@ let check_required_module ?loc sc (sp,d) =
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
 
-let find_with_delimiters = function
-  | None -> None
-  | Some scope ->
-      match (String.Map.find scope !scope_map).delimiters with
-	| Some key -> Some (Some scope, Some key)
-	| None -> None
-
-let rec find_without_delimiters find (ntn_scope,ntn) = function
-  | Scope scope :: scopes ->
+let rec find_without_delimiters find (istype,ntn_scope,ntn as ntndata) = function
+  | UninterpScope scope :: scopes ->
       (* Is the expected ntn/numpr attached to the most recently open scope? *)
       begin match ntn_scope with
       | Some scope' when String.equal scope scope' ->
-	Some (None,None)
+        Some None
       | _ ->
 	(* If the most recently open scope has a notation/numeral printer
     	   but not the expected one then we need delimiters *)
 	if find scope then
-	  find_with_delimiters ntn_scope
+          find_with_delimiters istype ntn_scope
 	else
-	  find_without_delimiters find (ntn_scope,ntn) scopes
+          find_without_delimiters find ntndata scopes
       end
-  | SingleNotation ntn' :: scopes ->
+  | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes ->
       begin match ntn_scope, ntn with
       | None, Some ntn when notation_eq ntn ntn' ->
-	Some (None, None)
+        Some None
       | _ ->
-	find_without_delimiters find (ntn_scope,ntn) scopes
+        find_without_delimiters find ntndata  scopes
       end
+  | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find ntndata  scopes
   | [] ->
       (* Can we switch to [scope]? Yes if it has defined delimiters *)
-      find_with_delimiters ntn_scope
+      find_with_delimiters istype ntn_scope
 
 (* The mapping between notations and their interpretation *)
 
@@ -902,9 +1031,19 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint =
   | Some _ -> ()
   end
 
+let scope_of_rule = function
+  | NotationRule (None,_) | SynDefRule _ -> None
+  | NotationRule (Some sc as sco,_) -> sco
+
+let uninterp_scope_to_add pat n = function
+  | NotationRule (None,_) | SynDefRule _ as rule -> Some (UninterpSingle (rule,pat,n))
+  | NotationRule (Some sc,_) -> None
+
 let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = notation_constr_key c in
-  notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
+  let sc = scope_of_rule rule in
+  notations_key_table := keymap_add key sc (rule,pat,n) !notations_key_table;
+  uninterp_scope_stack := Option.List.cons (uninterp_scope_to_add pat n rule) !uninterp_scope_stack
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
@@ -982,20 +1121,29 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
-let uninterp_notations c =
-  List.map_append (fun key -> keymap_find key !notations_key_table)
-    (glob_constr_keys c)
+let extract_notations (istype,scopes) keys =
+  if keys == [] then [] (* shortcut *) else
+  let scope_map, global_map = !notations_key_table in
+  let rec aux scopes seen =
+  match scopes with
+  | UninterpScope sc :: scopes -> keymap_extract istype keys sc scope_map @ aux scopes (String.Set.add sc seen)
+  | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen
+  | [] ->
+      let find key = try KeyMap.find key global_map with Not_found -> [] in
+      keymap_extract_remainder istype seen (List.flatten (List.map find keys))
+  in aux scopes String.Set.empty
 
-let uninterp_cases_pattern_notations c =
-  keymap_find (cases_pattern_key c) !notations_key_table
+let uninterp_notations scopes c =
+  let scopes = make_current_uninterp_scopes scopes in
+  extract_notations scopes (glob_constr_keys c)
 
-let uninterp_ind_pattern_notations ind =
-  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+let uninterp_cases_pattern_notations scopes c =
+  let scopes = make_current_uninterp_scopes scopes in
+  extract_notations scopes [cases_pattern_key c]
 
-let availability_of_notation (ntn_scope,ntn) scopes =
-  let f scope =
-    NotationMap.mem ntn (String.Map.find scope !scope_map).notations in
-  find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
+let uninterp_ind_pattern_notations scopes ind =
+  let scopes = make_current_uninterp_scopes scopes in
+  extract_notations scopes [RefKey (canonical_gr (IndRef ind))]
 
 (* We support coercions from a custom entry at some level to an entry
    at some level (possibly the same), and from and to the constr entry. E.g.:
@@ -1149,13 +1297,11 @@ let availability_of_prim_token n printer_scope local_scopes =
         | _ -> false
     with Not_found -> false
   in
-  let scopes = make_current_scopes local_scopes in
-  Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+  let istype,scopes = make_current_uninterp_scopes local_scopes in
+  find_without_delimiters f (istype,Some printer_scope,None) scopes
 
 (* Miscellaneous *)
 
-let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
-
 let notation_binder_source_eq s1 s2 = match s1, s2 with
 | NtnParsedAsIdent,  NtnParsedAsIdent -> true
 | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
@@ -1169,9 +1315,10 @@ let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeBinderList, NtnTypeBinderList -> true
 | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
-let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) =
+let var_attributes_eq (_, ((entry1, (tmpsc1, scl1)), tp1)) (_, ((entry2, (tmpsc2, scl2)), tp2)) =
   notation_entry_level_eq entry1 entry2 &&
-  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  Option.equal String.equal tmpsc1 tmpsc2 &&
+  List.equal String.equal scl1 scl2 &&
   ntpe_eq tp1 tp2
 
 let interpretation_eq (vars1, t1) (vars2, t2) =
@@ -1186,44 +1333,15 @@ let exists_notation_in_scope scopt ntn onlyprint r =
     interpretation_eq n.not_interp r
   with Not_found -> false
 
-let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
-
-(**********************************************************************)
-(* Mapping classes to scopes *)
-
-open Classops
-
-type scope_class = cl_typ
-
-let scope_class_compare : scope_class -> scope_class -> int =
-  cl_typ_ord
-
-let compute_scope_class sigma t =
-  let (cl,_,_) = find_class_type sigma t in
-  cl
-
-module ScopeClassOrd =
-struct
-  type t = scope_class
-  let compare = scope_class_compare
-end
-
-module ScopeClassMap = Map.Make(ScopeClassOrd)
-
-let initial_scope_class_map : scope_name ScopeClassMap.t =
-  ScopeClassMap.empty
-
-let scope_class_map = ref initial_scope_class_map
-
-let declare_scope_class sc cl =
-  scope_class_map := ScopeClassMap.add cl sc !scope_class_map
-
-let find_scope_class cl =
-  ScopeClassMap.find cl !scope_class_map
+let exists_notation_interpretation_in_scope scopt ntn =
+  let scope = match scopt with Some s -> s | None -> default_scope in
+  try
+    let sc = String.Map.find scope !scope_map in
+    let _ = NotationMap.find ntn sc.notations in
+    true
+  with Not_found -> false
 
-let find_scope_class_opt = function
-  | None -> None
-  | Some cl -> try Some (find_scope_class cl) with Not_found -> None
+let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
@@ -1245,9 +1363,6 @@ let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
 let compute_type_scope sigma t =
   find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
 
-let current_type_scope_name () =
-   find_scope_class_opt (Some CL_SORT)
-
 let scope_class_of_class (x : cl_typ) : scope_class =
   x
 
@@ -1604,7 +1719,7 @@ let locate_notation prglob ntn scope =
     str "Notation" ++ fnl () ++
     prlist_with_sep fnl (fun (ntn,l) ->
       let scope = find_default ntn scopes in
-      prlist
+      prlist_with_sep fnl
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
 	    pr_notation_info prglob df r ++
@@ -1667,17 +1782,18 @@ let pr_visibility prglob = function
 (* Synchronisation with reset *)
 
 let freeze _ =
- (!scope_map, !scope_stack, !arguments_scope,
+ (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope,
   !delimiters_map, !notations_key_table, !scope_class_map,
   !prim_token_interp_infos, !prim_token_uninterp_infos,
   !entry_coercion_map, !entry_has_global_map,
   !entry_has_ident_map)
 
-let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
+let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
   scope_map := scm;
   scope_stack := scs;
-  delimiters_map := dlm;
+  uninterp_scope_stack := uscs;
   arguments_scope := asc;
+  delimiters_map := dlm;
   notations_key_table := fkm;
   scope_class_map := clsc;
   prim_token_interp_infos := ptii;
@@ -1688,8 +1804,9 @@ let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) =
 
 let init () =
   init_scope_map ();
+  uninterp_scope_stack := [];
   delimiters_map := String.Map.empty;
-  notations_key_table := KeyMap.empty;
+  notations_key_table := (ScopeMap.empty,KeyMap.empty);
   scope_class_map := initial_scope_class_map;
   prim_token_interp_infos := String.Map.empty;
   prim_token_uninterp_infos := GlobRef.Map.empty
diff --git a/interp/notation.mli b/interp/notation.mli
index 734198bbf6..3480d1c8f2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -211,18 +211,28 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
 val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
 
-type notation_rule = interp_rule * interpretation * int option
+type notation_rule_core =
+    interp_rule (* kind of notation *)
+  * interpretation (* pattern associated to the notation *)
+  * int option (* number of expected arguments *)
+
+type notation_rule =
+    notation_rule_core
+  * delimiters option (* delimiter to possibly add *)
+  * bool (* true if the delimiter is mandatory *)
 
 (** Return the possible notations for a given term *)
-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
+val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list
+val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list
 
+(*
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
    argument is itself not None if a delimiters is needed *)
 val availability_of_notation : scope_name option * notation -> subscopes ->
   (scope_name option * delimiters option) option
+ *)
 
 (** {6 Miscellaneous} *)
 
@@ -233,6 +243,9 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
 val exists_notation_in_scope : scope_name option -> notation ->
       bool -> interpretation -> bool
 
+(** Checks for already existing notations *)
+val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool
+
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 6d65db9e22..5a548cfae4 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)%type".
+ "A -> list' A -> list' (A * A)".
 Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=
     Foo : foo A x
 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 94b86fc222..bec4fc1579 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
+(false && I 3)%bool /\ (I 6)%bool
      : 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 adab324cf0..2ffc3b14e2 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).
+Notation "! A" := (forall _:nat, A) (at level 60) : type_scope.
 
 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).
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope.
 
-Check (false && I 3)%bool /\ I 6.
+Check (false && I 3)%bool /\ (I 6)%bool.
 
 (**********************************************************************)
 (* Check notations with several recursive patterns                    *)
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index bcb2468792..923caedace 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -71,6 +71,7 @@ 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 48379f713d..f53313def9 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -128,25 +128,27 @@ 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
@@ -182,22 +184,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
@@ -209,17 +211,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
@@ -253,3 +255,17 @@ myfoo01 tt
      : nat
 myfoo01 tt
      : nat
+[{0; 0}]
+     : list (list nat)
+[{1; 2; 3};
+ {4; 5; 6};
+ {7; 8; 9}]
+     : list (list nat)
+Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
+     : unit
+
+amatch is not universe polymorphic
+Monomorphic alist = [0; 1; 2]
+     : list nat
+
+alist is not universe polymorphic
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 180e8d337e..15211f1233 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)).
+Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope.
 Check forall n:nat, {# n | 1 > n}.
 
 Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop.
@@ -183,9 +183,13 @@ 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).
@@ -193,10 +197,12 @@ 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").
+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.
 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) *)
@@ -410,3 +416,58 @@ 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 d25ad5dca8..d58e4bf2d6 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -21,3 +21,27 @@ 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
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 7800e91ee5..61206b6dd0 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).
-Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
+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 >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
 
@@ -94,3 +94,73 @@ Coercion App : expr >-> Funclass.
 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.