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

Ack-by: maximedenes

2 files changed, 9 insertions, 9 deletions

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