From fb30e8880a3027ef1c957df668a906d723e8a8a0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 May 2019 18:20:07 +0200
Subject: `deprecated` attribute support for notations and syntactic
 definitions

We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
---
 test-suite/bugs/closed/bug_4798.v | 5 -----
 test-suite/bugs/closed/bug_9166.v | 5 ++---
 2 files changed, 2 insertions(+), 8 deletions(-)
 delete mode 100644 test-suite/bugs/closed/bug_4798.v

(limited to 'test-suite/bugs')

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
-- 
cgit v1.2.3