diff options
| author | Hugo Herbelin | 2020-04-08 17:23:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-11 10:41:09 +0200 |
| commit | 33aaa5d64771c3644de4771338c371ce6b865647 (patch) | |
| tree | 9784941fee1c59152986afc988118d82a921c8de /test-suite | |
| parent | 9aefd708109658a8a17412e1fd7cc95bff454050 (diff) | |
If a custom entry has global, a bound variable is valid in this entry.
This is due to "global" being a syntactic notation, thus including ident.
Parsing was automatically supporting this. This commit adds support for printing.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 14 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 1 |
2 files changed, 9 insertions, 6 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 8948518b3b..f48eaac4c9 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -16,6 +16,8 @@ Entry constr:myconstr is : 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}] @@ -83,18 +85,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 225, 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 238, 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 242, 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 247, 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 @@ -103,9 +105,9 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 275, 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 279, 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 08a4480e8a..4d4b37a8b2 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -27,6 +27,7 @@ Check [ << # 0 >> ]. Axiom c : nat. Notation "x" := x (in custom myconstr at level 0, x global). Check [ b + c ]. +Check fun a => [ a + a ]. End A. |