From 3c83ca8b3ea9ec3ea6656dc7f726c46a21729541 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 08:52:29 +0000
Subject: [vernac] Generic parsing rules for attributes

---
 vernac/g_vernac.mlg | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'vernac')

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index bffdaa0b1..49fcda849 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -97,6 +97,20 @@ GRAMMAR EXTEND Gram
   | IDENT "local" -> VernacLocal true
   | IDENT "global" -> VernacLocal false
   | IDENT "coercion" -> VernacCoercion
+  | IDENT "deprecated" ; v = attribute_value ->
+    match v with
+    | `List [ k1, `Leaf since ; k2, `Leaf note ] when Names.Id.equal k1 (Names.Id.of_string "since") && Names.Id.equal k2 (Names.Id.of_string "note") -> VernacDeprecated (since, note)
+    |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+  ]]
+  ;
+  attribute_value:
+  [[ "=" ; v = string -> `Leaf v
+   | "(" ; m = LIST0 attribute_pair SEP "," ; ")" -> `List m
+   | -> `Empty
+  ]]
+  ;
+  attribute_pair:
+  [[ k = ident ; v = attribute_value -> (k, v)
   ]]
   ;
   vernac:
-- 
cgit v1.2.3