diff options
| author | Hugo Herbelin | 2020-02-10 22:31:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | 29919b725262dca76708192bde65ce82860747be (patch) | |
| tree | 61694625fbeb3491bef8cb1f09f2a07548318acf /test-suite | |
| parent | acde8140bd51be112be33ae07db68b2f3b93302c (diff) | |
Granting #9516 and #9518 (support for numerals and strings in custom entries).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 807914a671..1c8f237bb8 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 +[2 + 3] + : nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 2906698386..4ab800c9ba 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,6 +22,9 @@ 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 >> ]. +Notation "n" := n%nat (in custom myconstr at level 0, n bigint). +Check [ 2 + 3 ]. + End A. Module B. |