diff options
| author | Hugo Herbelin | 2019-12-30 17:18:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-11 09:25:55 +0200 |
| commit | 9aefd708109658a8a17412e1fd7cc95bff454050 (patch) | |
| tree | 06894101ea10b317d635b26dce0b5deca12d0561 /test-suite | |
| parent | 97aac6a7cf1bab3226f979b55e37d61f22c2f358 (diff) | |
If a custom entry has global, an argument-free abbreviation is valid in this entry.
Parsing was automatically supporting this. This commit adds support for printing.
Note: It would be more delicate to recognize that some given entry
support applicative nodes hence abbreviations with arguments.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 14 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 6 |
2 files changed, 14 insertions, 6 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index e121b5e86c..8948518b3b 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,6 +14,8 @@ Entry constr:myconstr is : nat [<< # 0 >>] : option nat +[b + c] + : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] @@ -81,18 +83,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 219, characters 0-160: +File "stdin", line 225, 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 238, 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 242, 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 247, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -101,9 +103,9 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 269, characters 0-61: +File "stdin", line 275, 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 279, 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..08a4480e8a 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,6 +22,12 @@ 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 ]. + End A. Module B. |