From c8b6081ebacc0dd8ee1527a271a380dbd3b859b9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Nov 2018 19:42:30 +0100
Subject: [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`.
---
 plugins/derive/g_derive.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/derive')

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)
 
 }
 
-- 
cgit v1.2.3