Merge PR #11694: Support printing argument-free abbreviations in custom entries with a global rule

Reviewed-by: ejgallego
Ack-by: gares

2 files changed, 17 insertions, 6 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index e121b5e86c..f48eaac4c9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,6 +14,10 @@ Entry constr:myconstr is
      : nat
 [<< # 0 >>]
      : option nat
+[b + c]
+     : nat
+fun a : nat => [a + a]
+     : nat -> nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
@@ -81,18 +85,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 219, characters 0-160:
+File "stdin", line 226, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 232, characters 0-60:
+File "stdin", line 239, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 236, characters 0-64:
+File "stdin", line 243, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 241, characters 0-62:
+File "stdin", line 248, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -101,9 +105,9 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 269, characters 0-61:
+File "stdin", line 276, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 273, characters 0-63:
+File "stdin", line 280, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 1cf0d919b1..4d4b37a8b2 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,6 +22,13 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
 Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
 Check [ << # 0 >> ].
 
+(* Now check with global *)
+
+Axiom c : nat.
+Notation "x" := x (in custom myconstr at level 0, x global).
+Check [ b + c ].
+Check fun a => [ a + a ].
+
 End A.
 
 Module B.