diff options
| author | Théo Zimmermann | 2019-06-12 14:03:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-12 14:03:37 +0200 |
| commit | 0ab76e968b9f3a02678ec8aa747da47f94181055 (patch) | |
| tree | 4c89a8d0e887c193979a8f61099c78c4aa6b2280 /test-suite/bugs | |
| parent | 0d4300771e4a6a26d948872262a79695a38c7e0d (diff) | |
| parent | 26ed9cb34ea5fc84fb086644a03d016817f30a4a (diff) | |
Merge PR #10180: `deprecated` attribute support for notations and syntactic definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/bug_4798.v | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9166.v | 5 |
2 files changed, 2 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v deleted file mode 100644 index f238086633..0000000000 --- a/test-suite/bugs/closed/bug_4798.v +++ /dev/null @@ -1,5 +0,0 @@ -(* DO NOT MODIFY THIS FILE DIRECTLY *) -(* It is autogenerated by dev/tools/update-compat.py. *) -Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.8"). -Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v index 21cd770cbb..cd594c660f 100644 --- a/test-suite/bugs/closed/bug_9166.v +++ b/test-suite/bugs/closed/bug_9166.v @@ -1,8 +1,7 @@ -(* DO NOT MODIFY THIS FILE DIRECTLY *) -(* It is autogenerated by dev/tools/update-compat.py. *) Set Warnings "+deprecated". -Notation bar := option (compat "8.8"). +#[deprecated(since = "X", note = "Y")] +Notation bar := option. Definition foo (x: nat) : nat := match x with |