diff options
| author | Emilio Jesus Gallego Arias | 2018-11-14 19:42:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 17:11:51 +0100 |
| commit | c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 (patch) | |
| tree | 622a359d4d1bc57b104ad042a9b1fc5e5d8d11fd /vernac/attributes.ml | |
| parent | 71938f0de10e1f3b69b1158b80b4898bf3a7dfdb (diff) | |
[vernacextend] Consolidate extension points API
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
Diffstat (limited to 'vernac/attributes.ml')
| -rw-r--r-- | vernac/attributes.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 88638b295b..bc0b0310b3 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -9,7 +9,14 @@ (************************************************************************) open CErrors -open Vernacexpr + +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags let unsupported_attributes = function | [] -> () |