Backport PR #12697: Fix bug #12691: an only-parsing notation needs to…

… produce a generic printing format in anticipation of further not-only-parsing uses of the notation

test-suite/output/Notations4.out

@@ -119,3 +119,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
+File "stdin", line 297, characters 0-30:
+Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
+0 :=: 0
+     : Prop

test-suite/output/Notations4.v

@@ -290,3 +290,11 @@ Check V tt.
 Check fun x : nat => V x.
 
 End O.
+
+Module Bug12691.
+
+Notation "x :=: y" := True (at level 70, no associativity, only parsing).
+Notation "x :=: y" := (x = y).
+Check (0 :=: 0).
+
+End Bug12691.

vernac/metasyntax.ml

@@ -1579,9 +1579,12 @@ let warn_irrelevant_format =
 
 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 {
+  let format =
+    if sd.only_parsing && sd.format <> None then (warn_irrelevant_format (); None)
+    else sd.format in
+  let pp_rule = make_pp_rule level sd.pp_syntax_data format in
+  (* We produce a generic rule even if this precise notation is only parsing *)
+  Some {
     synext_reserved = reserved;
     synext_unparsing = (pp_rule,level);
     synext_extra  = sd.extra;