Merge PR #12949: When a notation is only parsing, do not attach to it a specific format.

Reviewed-by: ejgallego

2 files changed, 18 insertions, 0 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"
+     ).