Addressing #6082 and #7766 (overriding format of notation).

We do two changes:
- We distinguish between a notion of format generically attached to
  notations and a new notion of format attached to interpreted
  notations. "Reserved Notation" attaches a format
  generically. "Notation" attaches the format specifically to the given
  interpretation, and additionally, attaches it generically if it is the
  first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
  a specific format.

20 files changed, 450 insertions, 184 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index a8d5ac610f..04419f08f7 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast,
 it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct
 definition is the following:
 
+.. coqtop:: none
+
+   Reset Initial.
+
 .. coqtop:: all
 
    Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99).
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index b96ef7c4e5..1d51109b7f 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -19,11 +19,17 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
 
+type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
 type notation_entry = InConstrEntry | InCustomEntry of string
 type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
 type notation_key = string
+
+(* A notation associated to a given parsing rule *)
 type notation = notation_entry_level * notation_key
 
+(* A notation associated to a given interpretation *)
+type specific_notation = notation_with_optional_scope * notation
+
 type 'a or_by_notation_r =
   | AN of 'a
   | ByNotation of (string * string option)
@@ -78,7 +84,7 @@ type cases_pattern_expr_r =
   (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
   | CPatAtom of qualid option
   | CPatOr   of cases_pattern_expr list
-  | CPatNotation of notation * cases_pattern_notation_substitution
+  | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution
     * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
                                   (notation n applied with substitution l1)
                                   applied to arguments l2 *)
@@ -119,7 +125,7 @@ and constr_expr_r =
   | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
   | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr Glob_term.cast_type
-  | CNotation of notation * constr_notation_substitution
+  | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
   | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
   | CDelimiters of string * constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index b4798127f9..401853b625 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -75,7 +75,8 @@ let rec cases_pattern_expr_eq p1 p2 =
     Option.equal qualid_eq r1 r2
   | CPatOr a1, CPatOr a2 ->
     List.equal cases_pattern_expr_eq a1 a2
-  | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
+  | CPatNotation (inscope1, n1, s1, l1), CPatNotation (inscope2, n2, s2, l2) ->
+    Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
     notation_eq n1 n2 &&
     cases_pattern_notation_substitution_eq s1 s2 &&
     List.equal cases_pattern_expr_eq l1 l2
@@ -160,7 +161,8 @@ let rec constr_expr_eq e1 e2 =
       Glob_ops.glob_sort_eq s1 s2
   | CCast(t1,c1), CCast(t2,c2) ->
     constr_expr_eq t1 t2 && cast_expr_eq c1 c2
-    | CNotation(n1, s1), CNotation(n2, s2) ->
+    | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
+      Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
       notation_eq n1 n2 &&
       constr_notation_substitution_eq s1 s2
     | CPrim i1, CPrim i2 ->
@@ -271,7 +273,7 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
   | CPatCstr (_,patl1,patl2) ->
     List.fold_left (cases_pattern_fold_names f)
       (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
-  | CPatNotation (_,(patl,patll),patl') ->
+  | CPatNotation (_,_,(patl,patll),patl') ->
     List.fold_left (cases_pattern_fold_names f)
       (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
   | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
@@ -320,7 +322,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
       f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
     | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
     | CCast (a,CastCoerce) -> f n acc a
-    | CNotation (_,(l,ll,bl,bll)) ->
+    | CNotation (_,_,(l,ll,bl,bll)) ->
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
@@ -399,9 +401,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CLetIn (na,a,t,b) ->
       CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
     | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
-    | CNotation (n,(l,ll,bl,bll)) ->
+    | CNotation (inscope,n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
-      CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
+      CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
                     List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
     | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
     | CDelimiters (s,a) -> CDelimiters (s,f e a)
@@ -574,7 +576,7 @@ let mkAppPattern ?loc p lp =
      CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern"
                       (Pp.str "Nested applications not supported.")
   | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
-  | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp)
+  | CPatNotation (inscope, n, s, l) -> CPatNotation (inscope, n , s, l@lp)
   | _ -> CErrors.user_err
            ?loc:p.loc ~hdr:"compound_pattern"
            (Pp.str "Such pattern cannot have arguments."))
@@ -591,8 +593,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
   | CAppExpl ((None,r,i),args) ->
      CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
-  | CNotation (ntn,(c,cl,[],[])) ->
-     CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c,
+  | CNotation (inscope,ntn,(c,cl,[],[])) ->
+     CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c,
                         List.map (List.map coerce_to_cases_pattern_expr) cl),[])
   | CPrim p ->
      CPatPrim p
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 06232b8e1a..a0f4bdcca1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -75,10 +75,10 @@ let inactive_notations_table =
 let inactive_scopes_table    =
   Summary.ref ~name:"inactive_scopes_table" CString.Set.empty
 
-let show_scope scopt =
-  match scopt with
-  | None -> str ""
-  | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc
+let show_scope inscope =
+  match inscope with
+  | LastLonelyNotation -> str ""
+  | NotationInScope sc -> spc () ++ str "in scope" ++ spc () ++ str sc
 
 let _show_inactive_notations () =
   begin
@@ -97,8 +97,8 @@ let _show_inactive_notations () =
     let _ = Feedback.msg_notice (str "Inactive notations:") in
     IRuleSet.iter
       (function
-       | NotationRule (scopt, ntn) ->
-         Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
+       | NotationRule (inscope, ntn) ->
+         Feedback.msg_notice (pr_notation ntn ++ show_scope inscope)
        | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
       !inactive_notations_table
 
@@ -107,18 +107,19 @@ let deactivate_notation nr =
   | SynDefRule kn ->
      (* shouldn't we check whether it is well defined? *)
      inactive_notations_table := IRuleSet.add nr !inactive_notations_table
-  | NotationRule (scopt, ntn) ->
-     match availability_of_notation (scopt, ntn) (scopt, []) with
+  | NotationRule (inscope, ntn) ->
+     let scopt = match inscope with NotationInScope sc -> Some sc | LastLonelyNotation -> None in
+     match availability_of_notation (inscope, ntn) (scopt, []) with
      | None -> 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 "."))
+                         ++ (match inscope with
+                             | LastLonelyNotation -> spc () ++ str "in the empty scope."
+                             | NotationInScope _ -> show_scope inscope ++ str "."))
      | Some _ ->
         if IRuleSet.mem nr !inactive_notations_table then
           Feedback.msg_warning
             (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
-             ++ str "is already inactive" ++ show_scope scopt ++ str ".")
+             ++ str "is already inactive" ++ show_scope inscope ++ str ".")
         else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
 
 let reactivate_notation nr =
@@ -127,9 +128,9 @@ let reactivate_notation nr =
       IRuleSet.remove nr !inactive_notations_table
   with Not_found ->
     match nr with
-    | NotationRule (scopt, ntn) ->
+    | NotationRule (inscope, ntn) ->
        Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
-                             ++ str "is already active" ++ show_scope scopt ++
+                             ++ str "is already active" ++ show_scope inscope ++
   str ".")
     | SynDefRule kn ->
        let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
@@ -157,8 +158,8 @@ let reactivate_scope sc =
 let is_inactive_rule nr =
   IRuleSet.mem nr !inactive_notations_table ||
   match nr with
-    | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
-    | NotationRule (None, ntn) -> false
+    | NotationRule (NotationInScope sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
+    | NotationRule (LastLonelyNotation, ntn) -> false
     | SynDefRule _ -> false
 
 (* args: notation, scope, activate/deactivate *)
@@ -169,10 +170,13 @@ let toggle_scope_printing ~scope ~activate =
     deactivate_scope scope
 
 let toggle_notation_printing ?scope ~notation ~activate =
+  let inscope = match scope with
+  | None -> LastLonelyNotation
+  | Some sc -> NotationInScope sc in
   if activate then
-    reactivate_notation (NotationRule (scope, notation))
+    reactivate_notation (NotationRule (inscope, notation))
   else
-    deactivate_notation (NotationRule (scope, notation))
+    deactivate_notation (NotationRule (inscope, notation))
 
 (* This governs printing of projections using the dot notation symbols *)
 let print_projections = ref false
@@ -254,11 +258,11 @@ let insert_pat_alias ?loc p = function
 
 let rec insert_coercion ?loc l c = match l with
   | [] -> c
-  | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[]))
+  | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[]))
 
 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],[]),[])
+  | (inscope,ntn)::l -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,([insert_pat_coercion ?loc l c],[]),[])
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -348,19 +352,19 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
            | None -> mknot (loc,ntn,l,bl) end
         | _ -> mknot (loc,ntn,l,bl)
 
-let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
+let make_notation loc (inscope,ntn) (terms,termlists,binders,binderlists as subst) =
   if not (List.is_empty termlists) || not (List.is_empty binderlists) then
-    CAst.make ?loc @@ CNotation (ntn,subst)
+    CAst.make ?loc @@ CNotation (Some inscope,ntn,subst)
   else
     make_notation_gen loc ntn
-      (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[])))
+      (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (Some inscope,ntn,(l,[],bl,[])))
       (fun (loc,p) -> CAst.make ?loc @@ CPrim p)
       destPrim terms binders
 
-let make_pat_notation ?loc ntn (terms,termlists as subst) args =
-  if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else
+let make_pat_notation ?loc (inscope,ntn) (terms,termlists as subst) args =
+  if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (Some inscope,ntn,subst,args)) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
+    (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,(l,[]),args))
     (fun (loc,p)     -> CAst.make ?loc @@ CPatPrim p)
     destPatPrim terms []
 
@@ -450,12 +454,12 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
 and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
     (custom, (tmp_scope, scopes) as allscopes) vars =
   function
-    | NotationRule (sc,ntn) ->
+    | NotationRule (_,ntn as specific_ntn) ->
       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
+        match availability_of_notation specific_ntn (tmp_scope,scopes) with
           (* Uninterpretation is not allowed in current context *)
           | None -> raise No_match
           (* Uninterpretation is allowed in current context *)
@@ -479,7 +483,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
             in
             insert_pat_coercion coercion
               (insert_pat_delimiters ?loc
-                 (make_pat_notation ?loc ntn (l,ll) l2') key)
+                 (make_pat_notation ?loc specific_ntn (l,ll) l2') key)
       end
     | SynDefRule kn ->
       match availability_of_entry_coercion custom InConstrEntrySomeLevel with
@@ -1185,11 +1189,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
           match_notation_constr !print_universes t pat in
         (* Try availability of interpretation ... *)
         match keyrule with
-          | NotationRule (sc,ntn) ->
+          | NotationRule (_,ntn as specific_ntn) ->
              (match availability_of_entry_coercion custom (fst ntn) with
              | None -> raise No_match
              | Some coercion ->
-               match availability_of_notation (sc,ntn) scopes with
+               match availability_of_notation specific_ntn scopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
@@ -1212,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                     List.map (fun (bl,(subentry,(scopt,scl))) ->
                       pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
                       binderlists in
-                  let c = make_notation loc ntn (l,ll,bl,bll) in
+                  let c = make_notation loc specific_ntn (l,ll,bl,bll) in
                   let c = insert_coercion coercion (insert_delimiters c key) in
                   let args = fill_arg_scopes args argsscopes allscopes in
                   let args = extern_args (extern true) vars args in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b2c572d290..1cfd50e26e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -226,7 +226,7 @@ let contract_curly_brackets ntn (l,ll,bl,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
+    | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -242,7 +242,7 @@ let contract_curly_brackets_pat ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
+    | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -1719,13 +1719,13 @@ let drop_notations_pattern looked_for genv =
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
+    | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
       let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
       rcp_of_glob scopes pat
-    | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
+    | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
       in_pat top scopes a
-    | CPatNotation (ntn,fullargs,extrargs) ->
+    | CPatNotation (_,ntn,fullargs,extrargs) ->
       let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
       let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
       let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
@@ -2035,11 +2035,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         DAst.make ?loc @@
         GLetIn (na.CAst.v, inc1, int,
           intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
-    | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
+    | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
        intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
-    | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
-    | CNotation (ntn,args) ->
+    | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
+    | CNotation (_,ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
     | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
@@ -2070,7 +2070,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             | CRef (ref,us) ->
                intern_applied_reference ~isproj intern env
                  (Environ.named_context_val globalenv) lvar us args ref
-            | CNotation (ntn,([],[],[],[])) ->
+            | CNotation (_,ntn,([],[],[],[])) ->
                 assert (Option.is_empty isproj);
                 let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index ffbb982ab7..e6f12f7eb2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let rec aux bdvars l c = match CAst.(c.v) with
     | CRef (qid,_) when qualid_is_ident qid ->
       found c.CAst.loc (qualid_basename qid) bdvars l
-    | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+    | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
         qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
         Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
diff --git a/interp/notation.ml b/interp/notation.ml
index 789d59eda9..744528ca0b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,6 +49,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
 | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
 
+let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with
+ | LastLonelyNotation, LastLonelyNotation -> true
+ | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2
+ | (LastLonelyNotation | NotationInScope _), _ -> false
+
 let notation_eq (from1,ntn1) (from2,ntn2) =
   notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
 
@@ -63,6 +68,15 @@ module NotationOrd =
 module NotationSet = Set.Make(NotationOrd)
 module NotationMap = CMap.Make(NotationOrd)
 
+module SpecificNotationOrd =
+  struct
+    type t = specific_notation
+    let compare = pervasives_compare
+  end
+
+module SpecificNotationSet = Set.Make(SpecificNotationOrd)
+module SpecificNotationMap = CMap.Make(SpecificNotationOrd)
+
 (**********************************************************************)
 (* Scope of symbols *)
 
@@ -254,7 +268,7 @@ let find_delimiters_scope ?loc key =
 (* Uninterpretation tables *)
 
 type interp_rule =
-  | NotationRule of scope_name option * notation
+  | NotationRule of specific_notation
   | SynDefRule of KerName.t
 
 (* We define keys for glob_constr and aconstr to split the syntax entries
@@ -1064,8 +1078,8 @@ let check_required_module ?loc sc (sp,d) =
    the scope stack [scopes], and if yes, using delimiters or not *)
 
 let find_with_delimiters = function
-  | None -> None
-  | Some scope ->
+  | LastLonelyNotation -> None
+  | NotationInScope scope ->
       match (String.Map.find scope !scope_map).delimiters with
         | Some key -> Some (Some scope, Some key)
         | None -> None
@@ -1074,7 +1088,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
   | OpenScopeItem 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' ->
+      | NotationInScope scope' when String.equal scope scope' ->
         Some (None,None)
       | _ ->
         (* If the most recently open scope has a notation/numeral printer
@@ -1086,7 +1100,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
       end
   | LonelyNotationItem ntn' :: scopes ->
       begin match ntn_scope, ntn with
-      | None, Some ntn when notation_eq ntn ntn' ->
+      | LastLonelyNotation, Some ntn when notation_eq ntn ntn' ->
         Some (None, None)
       | _ ->
         find_without_delimiters find (ntn_scope,ntn) scopes
@@ -1244,7 +1258,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
    commonly from the lowest level of the source entry to the highest
    level of the target entry. *)
 
-type entry_coercion = notation list
+type entry_coercion = (notation_with_optional_scope * notation) list
 
 module EntryCoercionOrd =
  struct
@@ -1295,7 +1309,7 @@ let rec insert_coercion_path path = function
       else if shorter_path path path' then path::allpaths
       else path'::insert_coercion_path path paths
 
-let declare_entry_coercion (entry,_ as ntn) entry' =
+let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
   let entry, lev = decompose_custom_entry entry in
   let entry', lev' = decompose_custom_entry entry' in
   (* Transitive closure *)
@@ -1304,19 +1318,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' =
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if notation_entry_eq entry entry''' && level_ord lev lev''' &&
            not (notation_entry_eq entry' entry'')
-        then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l)
+        then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
-        then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l)
+        then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
     List.fold_right (fun (pair,path) ->
         let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
         EntryCoercionMap.add pair (insert_coercion_path path olds))
-      (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft)
+      (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
       !entry_coercion_map
 
 let entry_has_global_map = ref String.Map.empty
@@ -1417,7 +1431,7 @@ let availability_of_prim_token n printer_scope local_scopes =
     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)
+  Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
 
 (* Miscellaneous *)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 707be6cb87..87f0ba63c8 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -25,11 +25,15 @@ val notation_entry_eq : notation_entry -> notation_entry -> bool
 val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
 (** Equality on [notation_entry_level]. *)
 
+val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_with_optional_scope -> bool
+
 val notation_eq : notation -> notation -> bool
 (** Equality on [notation]. *)
 
 module NotationSet : Set.S with type elt = notation
 module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet
+module SpecificNotationSet : Set.S with type elt = specific_notation
+module SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet
 
 (** {6 Scopes } *)
 (** A scope is a set of interpreters for symbols + optional
@@ -213,7 +217,7 @@ val availability_of_prim_token :
 
 (** Binds a notation in a given scope to an interpretation *)
 type interp_rule =
-  | NotationRule of scope_name option * notation
+  | NotationRule of specific_notation
   | SynDefRule of KerName.t
 
 val declare_notation_interpretation : notation -> scope_name option ->
@@ -236,7 +240,7 @@ 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
    argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> subscopes ->
+val availability_of_notation : specific_notation -> subscopes ->
   (scope_name option * delimiters option) option
 
 (** {6 Miscellaneous} *)
@@ -299,8 +303,8 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
-type entry_coercion = notation list
-val declare_entry_coercion : notation -> notation_entry_level -> unit
+type entry_coercion = (notation_with_optional_scope * notation) list
+val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
 val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
 
 val declare_custom_entry_has_global : string -> int -> unit
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index dcc3a87b11..d6c6c365cb 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -199,11 +199,11 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
             | CPrim (Numeral (SPlus,n)) ->
-                CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
+                CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
       | "{"; c = binder_constr ; "}" ->
-        { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
+        { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -380,7 +380,7 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           match p.CAst.v with
           | CPatPrim (Numeral (SPlus,n)) ->
-              CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+              CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c220abeda..915799e997 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -14,21 +14,23 @@ open Util
 open Notation
 open Notation_gram
 
-(* Uninterpreted notation levels *)
+(* Register the level of notation for parsing and printing
+   (we also register a precomputed parsing rule) *)
 
 let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
 
-let declare_notation_level ?(onlyprint=false) ntn level =
+let declare_notation_level ntn ~onlyprint parsing_rule level =
   try
-    let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
-    if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+    let _ = NotationMap.find ntn !notation_level_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
+  notation_level_map := NotationMap.add ntn (onlyprint,parsing_rule,level) !notation_level_map
 
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
+let level_of_notation ntn =
+  NotationMap.find ntn !notation_level_map
+
+let get_defined_notations () =
+  NotationSet.elements @@ NotationMap.domain !notation_level_map
 
 (**********************************************************************)
 (* Equality *)
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index c31f4505e7..d5711569f0 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -16,5 +16,9 @@ val level_eq : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
+val declare_notation_level : notation -> onlyprint:bool -> notation_grammar -> level -> unit
+val level_of_notation : notation -> bool (* = onlyprint *) * notation_grammar * level
+  (** raise [Not_found] if not declared *)
+
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 7368f4109e..92f44faec8 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -47,31 +47,56 @@ type unparsing =
 
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
+
+let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
+  | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2
+  | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2
+  | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
+  | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
+  | UnpCut p1, UnpCut p2 -> p1 = p2
+  | (UnpMetaVar _ | UnpBinderMetaVar _ | UnpListMetaVar _ |
+     UnpBinderListMetaVar _ | UnpTerminal _ | UnpBox _ | UnpCut _), _ -> false
+
 (* Concrete syntax for symbolic-extension table *)
-let notation_rules =
-  Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
+let generic_notation_printing_rules =
+  Summary.ref ~name:"generic-notation-printing-rules" (NotationMap.empty : (unparsing_rule * bool * extra_unparsing_rules) NotationMap.t)
+
+let specific_notation_printing_rules =
+  Summary.ref ~name:"specific-notation-printing-rules" (SpecificNotationMap.empty : (unparsing_rule * extra_unparsing_rules) SpecificNotationMap.t)
+
+let declare_generic_notation_printing_rules ntn ~reserved ~extra unpl =
+  generic_notation_printing_rules := NotationMap.add ntn (unpl,reserved,extra) !generic_notation_printing_rules
+let declare_specific_notation_printing_rules specific_ntn ~extra unpl =
+  specific_notation_printing_rules := SpecificNotationMap.add specific_ntn (unpl,extra) !specific_notation_printing_rules
+
+let has_generic_notation_printing_rule ntn =
+  NotationMap.mem ntn !generic_notation_printing_rules
+
+let find_generic_notation_printing_rule ntn =
+  NotationMap.find ntn !generic_notation_printing_rules
 
-let declare_notation_rule ntn ~extra unpl gram =
-  notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules
+let find_specific_notation_printing_rule specific_ntn =
+  SpecificNotationMap.find specific_ntn !specific_notation_printing_rules
 
-let find_notation_printing_rule ntn =
-  try pi1 (NotationMap.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
-let find_notation_extra_printing_rules ntn =
-  try pi2 (NotationMap.find ntn !notation_rules)
-  with Not_found -> []
-let find_notation_parsing_rules ntn =
-  try pi3 (NotationMap.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
+let find_notation_printing_rule which ntn =
+  try match which with
+  | None -> raise Not_found (* Normally not the case *)
+  | Some which -> fst (find_specific_notation_printing_rule (which,ntn))
+  with Not_found -> pi1 (find_generic_notation_printing_rule ntn)
 
-let get_defined_notations () =
-  NotationSet.elements @@ NotationMap.domain !notation_rules
+let find_notation_extra_printing_rules which ntn =
+  try match which with
+  | None -> raise Not_found
+  | Some which -> snd (find_specific_notation_printing_rule (which,ntn))
+  with Not_found -> pi3 (find_generic_notation_printing_rule ntn)
 
 let add_notation_extra_printing_rule ntn k v =
   try
-    notation_rules :=
-      let p, pp, gr = NotationMap.find ntn !notation_rules in
-      NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules
+    generic_notation_printing_rules :=
+      let p, b, pp = NotationMap.find ntn !generic_notation_printing_rules in
+      NotationMap.add ntn (p, b, (k,v) :: pp) !generic_notation_printing_rules
   with Not_found ->
     user_err ~hdr:"add_notation_extra_printing_rule"
       (str "No such Notation.")
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index be5af75e72..7996e7696d 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -41,11 +41,14 @@ type unparsing =
 
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
-val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
-val find_notation_parsing_rules : notation -> notation_grammar
-val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
-(** Returns notations with defined parsing/printing rules *)
-val get_defined_notations : unit -> notation list
+val unparsing_eq : unparsing -> unparsing -> bool
+
+val declare_generic_notation_printing_rules : notation -> reserved:bool -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_specific_notation_printing_rules : specific_notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val has_generic_notation_printing_rule : notation -> bool
+val find_generic_notation_printing_rule : notation -> unparsing_rule * bool * extra_unparsing_rules
+val find_specific_notation_printing_rule : specific_notation -> unparsing_rule * extra_unparsing_rules
+val find_notation_printing_rule : notation_with_optional_scope option -> notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation_with_optional_scope option -> notation -> extra_unparsing_rules
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index e45bae19ca..96f8cb12ba 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -857,7 +857,7 @@ let glob_cpattern gs p =
   | k, (v, Some t), _ as orig ->
      if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
      match t.CAst.v with
-     | CNotation((InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
+     | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ )"), ([t1; t2], [], [], [])) ->
          (try match glob t1, glob t2 with
          | (r1, None), (r2, None) -> encode k "In" [r1;r2]
          | (r1, Some _), (r2, Some _) when isCVar t1 ->
@@ -865,11 +865,11 @@ let glob_cpattern gs p =
          | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2]
          | _ -> CErrors.anomaly (str"where are we?.")
          with _ when isCVar t1 -> encode k "In" [bind_in t1 t2])
-     | CNotation((InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
+     | CNotation(_,(InConstrEntrySomeLevel,"( _ in _ in _ )"), ([t1; t2; t3], [], [], [])) ->
          check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3]
-     | CNotation((InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
+     | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ )"), ([t1; t2], [], [], [])) ->
          encode k "As" [fst (glob t1); fst (glob t2)]
-     | CNotation((InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
+     | CNotation(_,(InConstrEntrySomeLevel,"( _ as _ in _ )"), ([t1; t2; t3], [], [], [])) ->
          check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3]
      | _ -> glob_ssrterm gs orig
 ;;
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f9f46e1ceb..2f60663c82 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -133,8 +133,8 @@ let tag_var = tag Tag.variable
     in
     aux unps
 
-  let pr_notation pr pr_patt pr_binders s env =
-    let unpl, level = find_notation_printing_rule s in
+  let pr_notation pr pr_patt pr_binders which s env =
+    let unpl, level = find_notation_printing_rule which s in
     print_hunks level pr pr_patt pr_binders env unpl, level
 
   let pr_delimiters key strm =
@@ -279,11 +279,11 @@ let tag_var = tag Tag.variable
         let pp p = hov 0 (pr_patt mt (lpator,Any) p) in
         surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
 
-      | CPatNotation ((_,"( _ )"),([p],[]),[]) ->
+      | CPatNotation (_,(_,"( _ )"),([p],[]),[]) ->
         pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
 
-      | CPatNotation (s,(l,ll),args) ->
-        let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) s (l,ll,[],[]) in
+      | CPatNotation (which,s,(l,ll),args) ->
+        let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
         (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
         ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
 
@@ -650,10 +650,10 @@ let tag_var = tag Tag.variable
                     | CastCoerce -> str ":>"),
           lcast
         )
-      | CNotation ((_,"( _ )"),([t],[],[],[])) ->
+      | CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
         return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
-      | CNotation (s,env) ->
-        pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env
+      | CNotation (which,s,env) ->
+        pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env
       | CGeneralization (bk,ak,c) ->
         return (pr_generalization bk ak (pr mt ltop c), latom)
       | CPrim p ->
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index d93dd15f91..c3ee5968dc 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -529,7 +529,7 @@ let match_goals ot nt =
         constr_expr ogname a a2
       | CastCoerce, CastCoerce -> ()
       | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
-    | CNotation (ntn,args), CNotation (ntn2,args2) ->
+    | CNotation (_,ntn,args), CNotation (_,ntn2,args2) ->
       constr_notation_substitution ogname args args2
     | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
       constr_expr ogname c c2
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 1c8f237bb8..66b54b629f 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -77,3 +77,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 222, 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 235, characters 0-60:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 239, characters 0-64:
+Warning: Notation "_ %%% _" was already defined with a different format.
+[notation-incompatible-format,parsing]
+File "stdin", line 244, 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 272, characters 0-61:
+Warning: The format modifier is irrelevant for only parsing rules.
+[irrelevant-format-only-parsing,parsing]
+File "stdin", line 276, 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..a6503a8bf3 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -195,3 +195,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/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5e98f5ddc0..e8d0aee331 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -537,10 +537,10 @@ let rec pure_sublevels' assoc from forpat level = function
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
   let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in
-  CAst.make ~loc @@ CNotation (notation, env)
+  CAst.make ~loc @@ CNotation (None, notation, env)
 | ForPattern -> fun notation loc env ->
   let env = (env.constrs, env.constrlists) in
-  CAst.make ~loc @@ CPatNotation (notation, env, [])
+  CAst.make ~loc @@ CPatNotation (None, notation, env, [])
 
 let extend_constr state forpat ng =
   let custom,n,_,_ = ng.notgram_level in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f2e1002f71..623baf7db7 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -776,43 +776,96 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec =
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
 
-type syntax_extension = {
+let warn_incompatible_format =
+  CWarnings.create ~name:"notation-incompatible-format" ~category:"parsing"
+    (fun (specific,ntn) ->
+       let head,scope = match specific with
+       | None -> str "Notation", mt ()
+       | Some LastLonelyNotation -> str "Lonely notation", mt ()
+       | Some (NotationInScope sc) -> str "Notation", strbrk (" in scope " ^ sc) in
+       head ++ spc () ++ pr_notation ntn ++
+       strbrk " was already defined with a different format" ++ scope ++ str ".")
+
+type syntax_parsing_extension = {
   synext_level : Notation_gram.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
-  synext_unparsing : unparsing list;
+}
+
+type syntax_printing_extension = {
+  synext_reserved : bool;
+  synext_unparsing : unparsing_rule;
   synext_extra : (string * string) list;
 }
 
-type syntax_extension_obj = locality_flag * syntax_extension
+let generic_format_to_declare ntn {synext_unparsing = (rules,_); synext_extra = extra_rules } =
+  try
+    let (generic_rules,_),reserved,generic_extra_rules =
+      Ppextend.find_generic_notation_printing_rule ntn in
+    if reserved &&
+       (not (List.for_all2eq unparsing_eq rules generic_rules)
+       || extra_rules <> generic_extra_rules)
+    then
+      (warn_incompatible_format (None,ntn); true)
+    else
+      false
+  with Not_found -> true
+
+let check_reserved_format ntn = function
+  | None -> ()
+  | Some sy_pp_rules -> let _ = generic_format_to_declare ntn sy_pp_rules in ()
+
+let specific_format_to_declare (specific,ntn as specific_ntn)
+      {synext_unparsing = (rules,_); synext_extra = extra_rules } =
+  try
+    let (specific_rules,_),specific_extra_rules =
+      Ppextend.find_specific_notation_printing_rule specific_ntn in
+    if not (List.for_all2eq unparsing_eq rules specific_rules)
+       || extra_rules <> specific_extra_rules then
+      (warn_incompatible_format (Some specific,ntn); true)
+    else false
+  with Not_found -> true
+
+type syntax_extension_obj =
+  locality_flag * (syntax_parsing_extension * syntax_printing_extension option)
 
 let check_and_extend_constr_grammar ntn rule =
   try
     let ntn_for_grammar = rule.notgram_notation in
     if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
-    let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
-    if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+    let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
+    if not (Notgram_ops.level_eq prec oldprec) && not oldonlyprint then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+    if oldonlyprint then raise Not_found
   with Not_found ->
     Egramcoq.extend_constr_grammar rule
 
-let cache_one_syntax_extension se =
-  let ntn = se.synext_notation in
-  let prec = se.synext_level in
-  let onlyprint = se.synext_notgram.notgram_onlyprinting in
-  try
-    let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
-    if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
-  with Not_found ->
-    begin
-      (* Reserve the notation level *)
-      Notgram_ops.declare_notation_level ntn prec ~onlyprint;
-      (* Declare the parsing rule *)
-      if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
-      (* Declare the notation rule *)
-      declare_notation_rule ntn
-        ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
-    end
+let cache_one_syntax_extension (pa_se,pp_se) =
+  let ntn = pa_se.synext_notation in
+  let prec = pa_se.synext_level in
+  let onlyprint = pa_se.synext_notgram.notgram_onlyprinting in
+  (* Check and ensure that the level and the precomputed parsing rule is declared *)
+  let parsing_to_activate =
+    try
+      let oldonlyprint,_,oldprec = Notgram_ops.level_of_notation ntn in
+      if not (Notgram_ops.level_eq prec oldprec) && (not oldonlyprint || onlyprint) then error_incompatible_level ntn oldprec prec;
+      oldonlyprint && not onlyprint
+    with Not_found ->
+      (* Declare the level and the precomputed parsing rule *)
+      let _ = Notgram_ops.declare_notation_level ntn ~onlyprint pa_se.synext_notgram prec in
+      not onlyprint in
+  (* Declare the parsing rule *)
+  if parsing_to_activate then
+    List.iter (check_and_extend_constr_grammar ntn) pa_se.synext_notgram.notgram_rules;
+  (* Printing *)
+  match pp_se with
+  | None -> ()
+  | Some pp_se ->
+    (* Check compatibility of format in case of two Reserved Notation *)
+    (* and declare or redeclare printing rule *)
+    if generic_format_to_declare ntn pp_se then
+      declare_generic_notation_printing_rules ntn
+        ~extra:pp_se.synext_extra ~reserved:pp_se.synext_reserved pp_se.synext_unparsing
 
 let cache_syntax_extension (_, (_, sy)) =
   cache_one_syntax_extension sy
@@ -821,11 +874,11 @@ let subst_parsing_rule subst x = x
 
 let subst_printing_rule subst x = x
 
-let subst_syntax_extension (subst, (local, sy)) =
-  (local, { sy with
-    synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules };
-    synext_unparsing = subst_printing_rule subst sy.synext_unparsing;
-  })
+let subst_syntax_extension (subst, (local, (pa_sy,pp_sy))) =
+  (local, ({ pa_sy with
+    synext_notgram = { pa_sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) pa_sy.synext_notgram.notgram_rules }},
+    Option.map (fun pp_sy -> {pp_sy with synext_unparsing = subst_printing_rule subst pp_sy.synext_unparsing}) pp_sy)
+  )
 
 let classify_syntax_definition (local, _ as o) =
   if local then Dispose else Substitute o
@@ -1351,6 +1404,7 @@ type notation_obj = {
   notobj_onlyprint : bool;
   notobj_deprecation : Deprecation.t option;
   notobj_notation : notation * notation_location;
+  notobj_specific_pp_rules : syntax_printing_extension option;
 }
 
 let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
@@ -1372,22 +1426,31 @@ let open_notation i (_, nobj) =
   let pat = nobj.notobj_interp in
   let onlyprint = nobj.notobj_onlyprint  in
   let deprecation = nobj.notobj_deprecation in
+  let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+  let specific_ntn = (specific,ntn) in
   let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
   if Int.equal i 1 && fresh then begin
     (* Declare the interpretation *)
     let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
     (* Declare the uninterpretation *)
     if not nobj.notobj_onlyparse then
-      Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
+      Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
     (* Declare a possible coercion *)
     (match nobj.notobj_coercion with
-    | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion ntn entry
+    | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
     | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
     | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
     | Some (IsEntryNumeral (entry,n)) -> Notation.declare_custom_entry_has_numeral entry n
     | Some (IsEntryString (entry,n)) -> Notation.declare_custom_entry_has_string entry n
     | None -> ())
-  end
+  end;
+  (* Declare specific format if any *)
+  match nobj.notobj_specific_pp_rules with
+  | Some pp_sy ->
+    if specific_format_to_declare specific_ntn pp_sy then
+      Ppextend.declare_specific_notation_printing_rules
+        specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+  | None -> ()
 
 let cache_notation o =
   load_notation_common false 1 o;
@@ -1428,22 +1491,27 @@ let with_syntax_protection f x =
 exception NoSyntaxRule
 
 let recover_notation_syntax ntn =
-  try
-    let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
-    let pp_rule,_ = find_notation_printing_rule ntn in
-    let pp_extra_rules = find_notation_extra_printing_rules ntn in
-    let pa_rule = find_notation_parsing_rules ntn in
-    { synext_level = prec;
-      synext_notation = ntn;
-      synext_notgram = pa_rule;
-      synext_unparsing = pp_rule;
-      synext_extra = pp_extra_rules;
-    }
-  with Not_found ->
-    raise NoSyntaxRule
+  let pa =
+    try
+      let _,pa_rule,prec = Notgram_ops.level_of_notation ntn in
+      { synext_level = prec;
+        synext_notation = ntn;
+        synext_notgram = pa_rule }
+    with Not_found ->
+      raise NoSyntaxRule in
+  let pp =
+    try
+      let pp_rule,reserved,pp_extra_rules = find_generic_notation_printing_rule ntn in
+      Some {
+        synext_reserved = reserved;
+        synext_unparsing = pp_rule;
+        synext_extra = pp_extra_rules;
+      }
+    with Not_found -> None in
+  pa,pp
 
 let recover_squash_syntax sy =
-  let sq = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
+  let sq,_ = recover_notation_syntax (InConstrEntrySomeLevel,"{ _ }") in
   sy :: sq.synext_notgram.notgram_rules
 
 (**********************************************************************)
@@ -1475,16 +1543,25 @@ let make_pp_rule level (typs,symbols) fmt =
   | Some fmt ->
      hunks_of_format (level, List.split typs) (symbols, parse_format fmt)
 
-(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
-let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
+let make_parsing_rules (sd : SynData.syn_data) = let open SynData in
   let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
-  let custom,level,_,_ = sd.level in
-  let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
-  let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in {
+  let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in {
     synext_level    = sd.level;
     synext_notation = fst sd.info;
     synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
-    synext_unparsing = pp_rule;
+  }
+
+let warn_irrelevant_format =
+  CWarnings.create ~name:"irrelevant-format-only-parsing" ~category:"parsing"
+    (fun () -> str "The format modifier is irrelevant for only parsing rules.")
+
+let make_printing_rules reserved (sd : SynData.syn_data) = let open SynData in
+  let custom,level,_,_ = sd.level in
+  let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in
+  if sd.only_parsing then (if sd.format <> None then warn_irrelevant_format (); None)
+  else Some {
+    synext_reserved = reserved;
+    synext_unparsing = (pp_rule,level);
     synext_extra  = sd.extra;
   }
 
@@ -1498,9 +1575,10 @@ let to_map l =
 let add_notation_in_scope ~local deprecation df env c mods scope =
   let open SynData in
   let sd = compute_syntax_data ~local deprecation df mods in
-  (* Prepare the interpretation *)
   (* Prepare the parsing and printing rules *)
-  let sy_rules = make_syntax_rules sd in
+  let sy_pa_rules = make_parsing_rules sd in
+  let sy_pp_rules = make_printing_rules false sd in
+  (* Prepare the interpretation *)
   let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in
   let nenv = {
     ninterp_var_type = to_map i_vars;
@@ -1520,24 +1598,29 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
     notobj_onlyprint = sd.only_printing;
     notobj_deprecation = sd.deprecation;
     notobj_notation = sd.info;
+    notobj_specific_pp_rules = sy_pp_rules;
   } in
+  let gen_sy_pp_rules =
+    if Ppextend.has_generic_notation_printing_rule (fst sd.info) then None
+    else sy_pp_rules (* We use the format of this notation as the default *) in
+  let _ = check_reserved_format (fst sd.info) sy_pp_rules in
   (* Ready to change the global state *)
   List.iter (fun f -> f ()) sd.msgs;
-  Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules));
+  Lib.add_anonymous_leaf (inSyntaxExtension (local, (sy_pa_rules,gen_sy_pp_rules)));
   Lib.add_anonymous_leaf (inNotation notation);
   sd.info
 
 let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
-  let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
-    let sy = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
+  let level, i_typs, onlyprint, pp_sy = if not (is_numeral symbs) then begin
+    let (pa_sy,pp_sy as sy) = recover_notation_syntax (make_notation_key InConstrEntrySomeLevel symbs) in
     let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (* If the only printing flag has been explicitly requested, put it back *)
-    let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
-    let _,_,_,typs = sy.synext_level in
-    Some sy.synext_level, typs, onlyprint
-  end else None, [], false in
+    let onlyprint = onlyprint || pa_sy.synext_notgram.notgram_onlyprinting in
+    let _,_,_,typs = pa_sy.synext_level in
+    Some pa_sy.synext_level, typs, onlyprint, pp_sy
+  end else None, [], false, None in
   (* Declare interpretation *)
   let path = (Lib.library_dp(), Lib.current_dirpath true) in
   let df'  = (make_notation_key InConstrEntrySomeLevel symbs, (path,df)) in
@@ -1560,6 +1643,7 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
     notobj_onlyprint = onlyprint;
     notobj_deprecation = deprecation;
     notobj_notation = df';
+    notobj_specific_pp_rules = pp_sy;
   } in
   Lib.add_anonymous_leaf (inNotation notation);
   df'
@@ -1567,10 +1651,11 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
 (* Notations without interpretation (Reserved Notation) *)
 
 let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
-  let psd = compute_pure_syntax_data ~local df mods in
-  let sy_rules = make_syntax_rules {psd with deprecation = None} in
+  let psd = {(compute_pure_syntax_data ~local df mods) with deprecation = None} in
+  let pa_rules = make_parsing_rules psd in
+  let pp_rules = make_printing_rules true psd in
   List.iter (fun f -> f ()) psd.msgs;
-  Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
+  Lib.add_anonymous_leaf (inSyntaxExtension(local,(pa_rules,pp_rules)))
 
 (* Notations with only interpretation *)