diff options
| author | Hugo Herbelin | 2020-02-19 21:09:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-19 21:09:53 +0100 |
| commit | 25cab58df1171c9419396342e9ecc3094b74eca5 (patch) | |
| tree | 3bca55801e7915c333af55a5f876a869499d7d70 /test-suite | |
| parent | 43c3c7d6f62a9bee4772242c27fbafd54770d271 (diff) | |
Revert "Granting #9516 and #9518 (support for numerals and strings in custom entries)."
This reverts commit 29919b725262dca76708192bde65ce82860747be.
It was pushed by mistake as part of #11530. Sorry about it.
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, 0 insertions, 5 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 1c8f237bb8..807914a671 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -14,8 +14,6 @@ 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 4ab800c9ba..2906698386 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -22,9 +22,6 @@ 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. |