Merge 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

Reviewed-by: ppedrot

3 files changed, 18 insertions, 3 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 9cb019ca56..fa03ec8193 100644
--- a/test-suite/output/Notations4.out
+++ b/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
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b3270d4f92..90d8da2bec 100644
--- a/test-suite/output/Notations4.v
+++ b/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.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e9b86f323b..6cc48d0e48 100644
--- a/vernac/metasyntax.ml
+++ b/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;