Adapt to rocq-prover/rocq#21107

Author: proux01

test-suite/output/BinaryPrintingNotations.out

@@ -32,6 +32,9 @@ The command has indeed failed with message:
 Notations for numbers or strings are primitive and need not be reserved.
 "t""t"
      : unit
+File "./output/NotationSyntax.v", line 25, characters 0-60:
+Warning: Notations at level 0 should be closed (first and last symbols should
+be terminal symbols). [level-0-notation-not-closed,parsing,default]
 # "|" true
      : option bool
 "|"%string

test-suite/output/NotationSyntax.out

@@ -1,3 +1,6 @@
+File "./output/allBytes.v", line 18, characters 0-94:
+Warning: Notations at level 0 should be closed (first and last symbols should
+be terminal symbols). [level-0-notation-not-closed,parsing,default]
 File "./output/allBytes.v", line 23, characters 0-44:
 Warning: Lonely notation "" was already defined with a different format.
 [notation-incompatible-format,parsing,default]

test-suite/output/allBytes.out

@@ -138,6 +138,10 @@ i : Choose false -> Union (M A)
 
 fi fu : B
      : B
+File "./output/bug_13942.v", line 204, characters 0-113:
+Warning: Closed notations (i.e. starting and ending with a terminal symbol)
+should usually be at level 0 (default).
+[closed-notation-not-level-0,parsing,default]
 File "./output/bug_13942.v", line 307, characters 20-31:
 The command has indeed failed with message:
 Could not find an instance for "Insert K K (M A)" in