When a notation is only parsing, do not attach to it a specific format.

3 files changed, 26 insertions, 5 deletions

diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/bug_9682.out
diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v
new file mode 100644
index 0000000000..3630142126
--- /dev/null
+++ b/test-suite/output/bug_9682.v
@@ -0,0 +1,18 @@
+Declare Scope blafu.
+Delimit Scope blafu with B.
+Axiom DoesNotMatch : Type.
+Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit.
+
+Notation "|  p1  |  ..  |  pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu.
+Notation "'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" :=
+    (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
+      (at level 200, ls at level 91, only parsing).
+Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
+  (mmatch_do_not_write x in T as y return M p with_do_not_write ls)
+    (at level 200, ls at level 91, p at level 10, only parsing).
+(* This should not gives a warning *)
+Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" :=
+  (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B)
+    (at level 200, ls at level 91, p at level 10, only printing,
+     format "'[  ' mmatch  '/' x ']'  '/' '[  ' in  '/' T ']'  '/' '[  ' as  '/' y ']'  '/' '[  ' return  M  p ']'  with  '//' '[' ls ']'  '//' end"
+     ).
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 0bdcd53c92..45cc7894c1 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1608,7 +1608,14 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   let sd = compute_syntax_data ~local deprecation df mods in
   (* Prepare the parsing and printing rules *)
   let sy_pa_rules = make_parsing_rules sd in
-  let sy_pp_rules = make_printing_rules false sd in
+  let sy_pp_rules, gen_sy_pp_rules =
+    match sd.only_parsing, Ppextend.has_generic_notation_printing_rule (fst sd.info) with
+    | true, true -> None, None
+    | onlyparse, has_generic ->
+      let rules = make_printing_rules false sd in
+      let _ = check_reserved_format (fst sd.info) rules in
+      (if onlyparse then None else rules),
+      (if has_generic then None else (* We use the format of this notation as the default *) rules) in
   (* Prepare the interpretation *)
   let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in
   let nenv = {
@@ -1632,10 +1639,6 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
     notobj_notation = (notation, location);
     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_pa_rules,gen_sy_pp_rules)));