[vernac] Generic syntax for flags/attributes

1 files changed, 17 insertions, 25 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 49fcda849..92c685741 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -87,50 +87,42 @@ GRAMMAR EXTEND Gram
   | fv = vernac -> fv
   ]]
   ;
-  attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]]
-  ;
-  attribute:
-  [[
-    IDENT "polymorphic" -> VernacPolymorphic true
-  | IDENT "monomorphic" -> VernacPolymorphic false
-  | IDENT "program" -> VernacProgram
-  | 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")
+  attributes:
+  [[ "#[" ; a = attribute_list ; "]" -> a
   ]]
   ;
-  attribute_value:
-  [[ "=" ; v = string -> `Leaf v
-   | "(" ; m = LIST0 attribute_pair SEP "," ; ")" -> `List m
-   | -> `Empty
+  attribute_list:
+  [[ a = LIST0 attribute SEP "," -> a
   ]]
   ;
-  attribute_pair:
+  attribute:
   [[ k = ident ; v = attribute_value -> (k, v)
   ]]
   ;
+  attribute_value:
+  [[ "=" ; v = string -> VernacFlagLeaf v
+   | "(" ; a = attribute_list ; ")" -> VernacFlagList a
+   | -> VernacFlagEmpty
+  ]]
+  ;
   vernac:
-    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) }
-      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) }
+    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "local", VernacFlagEmpty) :: f, v) }
+      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "global", VernacFlagEmpty) :: f, v) }
 
       | v = vernac_poly -> { v } ]
     ]
   ;
   vernac_poly:
-    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic true :: f, v) }
-      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic false :: f, v) }
+    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "polymorphic", VernacFlagEmpty) :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "monomorphic", VernacFlagEmpty) :: f, v) }
       | v = vernac_aux -> { v } ]
     ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> { ([VernacProgram], g) }
-      | IDENT "Program"; g = gallina_ext; "." -> { ([VernacProgram], g) }
+    [ [ IDENT "Program"; g = gallina; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
+      | IDENT "Program"; g = gallina_ext; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
       | g = gallina; "." -> { ([], g) }
       | g = gallina_ext; "." -> { ([], g) }
       | c = command; "." -> { ([], c) }