From 5494c46f6219bea902fcc5ed983e16d1105fec51 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 08:00:47 +0000
Subject: [vernac] Add a “deprecated” attribute
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 vernac/vernacentries.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'vernac/vernacentries.ml')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1740c5a80..af0f19834 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2335,6 +2335,10 @@ let attributes_of_flags f atts =
          (polymorphism, { atts with locality = Some b })
        | VernacLocal _ ->
          user_err Pp.(str "Locality specified twice")
+       | VernacDeprecated (since, note) when Option.is_empty atts.deprecated ->
+         (polymorphism, { atts with deprecated = Some (since, note) })
+       | VernacDeprecated _ ->
+         user_err Pp.(str "Deprecation specified twice")
     )
     (None, atts)
     f
-- 
cgit v1.2.3