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/vernacexpr.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/vernacexpr.ml')

diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index f5f37339c..57ccb6006 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -463,6 +463,7 @@ type nonrec vernac_flag =
   | VernacProgram
   | VernacPolymorphic of bool
   | VernacLocal of bool
+  | VernacDeprecated of string * string (* Since, Note *)
 
 type vernac_control =
   | VernacExpr of vernac_flag list * vernac_expr
-- 
cgit v1.2.3