diff options
| author | Hugo Herbelin | 2020-02-15 18:42:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-16 21:44:43 +0100 |
| commit | 6a630e92a2c0972d78e724482c71b1f7f7232369 (patch) | |
| tree | 61694625fbeb3491bef8cb1f09f2a07548318acf /test-suite | |
| parent | 96e78e7e25d666f30a7c00e0288762e127690c67 (diff) | |
Revert "Suite picking numeral notation"
This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index dbfa939230..4ab800c9ba 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -25,20 +25,6 @@ Check [ << # 0 >> ]. Notation "n" := n%nat (in custom myconstr at level 0, n bigint). Check [ 2 + 3 ]. -Module A1. - (* This is compatible with bigint *) - Notation "x" := x (in custom myconstr at level 0, x ident). - (* This is incompatible with ident *) - Fail Notation "x" := x (in custom myconstr at level 0, x global). -End A1. - -Module A2. - (* This is compatible with bigint *) - Notation "x" := x (in custom myconstr at level 0, x global). - (* This is compatible with bigint and global *) - Notation "x" := x (in custom myconstr at level 0, x string). -End A2. - End A. Module B. |