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 /plugins/derive | |
| 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 'plugins/derive')
| -rw-r--r-- | plugins/derive/g_derive.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 18316bf2cd..df4b647642 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) } |