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`.
---
 coqpp/coqpp_main.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'coqpp')

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index ba3b9bcbbf..8da4c6db13 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -374,9 +374,9 @@ let print_rules fmt rules =
 let print_classifier fmt = function
 | ClassifDefault -> fprintf fmt ""
 | ClassifName "QUERY" ->
-  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_query)"
+  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_query)"
 | ClassifName "SIDEFF" ->
-  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_sideeff)"
+  fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_sideeff)"
 | ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
 | ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
 
-- 
cgit v1.2.3