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/funind/g_indfun.mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 155df1c1e0..7e707b423a 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,8 +186,8 @@ VERNAC COMMAND EXTEND Function
            Vernac_classifier.classify_vernac
              (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
          with
-         | Vernacexpr.VtSideff ids, _ when hard ->
-             Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+         | Vernacextend.VtSideff ids, _ when hard ->
+             Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
          | x -> x }
     -> { do_generate_principle false (List.map snd recsl) }
 END
@@ -225,7 +225,7 @@ let warning_error names e =
 
 VERNAC COMMAND EXTEND NewFunctionalScheme
 | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
-   => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater }
+   => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     {
       begin
@@ -261,7 +261,7 @@ END
 
 VERNAC COMMAND EXTEND NewFunctionalCase
 | ["Functional" "Case" fun_scheme_arg(fas) ]
-  => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater }
+  => { Vernacextend.(VtSideff[pi1 fas], VtLater) }
   -> { Functional_principles_types.build_case_scheme fas }
 END
 
-- 
cgit v1.2.3