Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation format + new notion of format associated to a given interpretation

Ack-by: maximedenes

7 files changed, 118 insertions, 88 deletions

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 c198c4eb9b..0a3ee59f4e 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
@@ -1183,11 +1187,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 *)
@@ -1210,7 +1214,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 93969f3718..2086e08f79 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 *)
 
@@ -148,21 +162,21 @@ let normalize_scope sc =
 (**********************************************************************)
 (* The global stack of scopes                                         *)
 
-type scope_elem = Scope of scope_name | SingleNotation of notation
-type scopes = scope_elem list
+type scope_item = OpenScopeItem of scope_name | LonelyNotationItem of notation
+type scopes = scope_item list
 
 let scope_eq s1 s2 = match s1, s2 with
-| Scope s1, Scope s2 -> String.equal s1 s2
-| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2
-| Scope _, SingleNotation _
-| SingleNotation _, Scope _ -> false
+| OpenScopeItem s1, OpenScopeItem s2 -> String.equal s1 s2
+| LonelyNotationItem s1, LonelyNotationItem s2 -> notation_eq s1 s2
+| OpenScopeItem _, LonelyNotationItem _
+| LonelyNotationItem _, OpenScopeItem _ -> false
 
 let scope_stack = ref []
 
 let current_scopes () = !scope_stack
 
 let scope_is_open_in_scopes sc l =
-  List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l
+  List.exists (function OpenScopeItem sc' -> String.equal sc sc' | _ -> false) l
 
 let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 
@@ -188,7 +202,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_item -> obj =
   declare_object {(default_object "SCOPE") with
       cache_function = cache_scope;
       open_function = open_scope;
@@ -197,11 +211,11 @@ 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,OpenScopeItem (normalize_scope sc)))
 
 let empty_scope_stack = []
 
-let push_scope sc scopes = Scope sc :: scopes
+let push_scope sc scopes = OpenScopeItem sc :: scopes
 
 let push_scopes = List.fold_right push_scope
 
@@ -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,17 +1078,17 @@ 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
 
 let rec find_without_delimiters find (ntn_scope,ntn) = function
-  | Scope scope :: scopes ->
+  | 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
@@ -1084,9 +1098,9 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
         else
           find_without_delimiters find (ntn_scope,ntn) scopes
       end
-  | SingleNotation ntn' :: scopes ->
+  | 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
@@ -1123,7 +1137,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
     scope_map := String.Map.add scope sc !scope_map
   end;
   begin match scopt with
-  | None -> scope_stack := SingleNotation ntn :: !scope_stack
+  | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack
   | Some _ -> ()
   end
 
@@ -1133,15 +1147,15 @@ let declare_uninterpretation rule (metas,c as pat) =
 
 let rec find_interpretation ntn find = function
   | [] -> raise Not_found
-  | Scope scope :: scopes ->
+  | OpenScopeItem scope :: scopes ->
       (try let n = find scope in (n,Some scope)
        with Not_found -> find_interpretation ntn find scopes)
-  | SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
+  | LonelyNotationItem ntn'::scopes when notation_eq ntn' ntn ->
       (try let n = find default_scope in (n,None)
        with Not_found ->
          (* e.g. because single notation only for constr, not cases_pattern *)
          find_interpretation ntn find scopes)
-  | SingleNotation _::scopes ->
+  | LonelyNotationItem _::scopes ->
       find_interpretation ntn find scopes
 
 let find_notation ntn sc =
@@ -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
@@ -1389,7 +1403,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 *)
 
@@ -1705,11 +1719,11 @@ let pr_scopes prglob =
 
 let rec find_default ntn = function
   | [] -> None
-  | Scope scope :: scopes ->
+  | OpenScopeItem scope :: scopes ->
     if NotationMap.mem ntn (find_scope scope).notations then
       Some scope
     else find_default ntn scopes
-  | SingleNotation ntn' :: scopes ->
+  | LonelyNotationItem ntn' :: scopes ->
     if notation_eq ntn ntn' then Some default_scope
     else find_default ntn scopes
 
@@ -1863,13 +1877,13 @@ let collect_notation_in_scope scope sc known =
 let collect_notations stack =
   fst (List.fold_left
     (fun (all,knownntn as acc) -> function
-      | Scope scope ->
+      | OpenScopeItem scope ->
           if String.List.mem_assoc scope all then acc
           else
             let (l,knownntn) =
               collect_notation_in_scope scope (find_scope scope) knownntn in
             ((scope,l)::all,knownntn)
-      | SingleNotation ntn ->
+      | LonelyNotationItem ntn ->
           if List.mem_f notation_eq ntn knownntn then (all,knownntn)
           else
           try
diff --git a/interp/notation.mli b/interp/notation.mli
index ea5125f7ec..26c45d5896 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