diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-25 08:52:29 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:01:20 +0000 |
| commit | 3c83ca8b3ea9ec3ea6656dc7f726c46a21729541 (patch) | |
| tree | e4f11aa084d1a24ec7154c3a08811e51f4d995f8 /vernac | |
| parent | 5494c46f6219bea902fcc5ed983e16d1105fec51 (diff) | |
[vernac] Generic parsing rules for attributes
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 14 |
1 files changed, 14 insertions, 0 deletions
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: |