From 4aa99307874c59f97570f624a06463aaa8115ec5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Nov 2018 14:25:33 +0100
Subject: [vernac] Rename Vernacinterp to Vernacextend and move extension
 functions there.

This PR fixes an issues that was bugging me for some time, namely that
`Vernacinterp` really means `Vernacextend`.

We thus rename the file and move the associated functions there, which
were incorrectly placed in `Vernacentries`.

Note the beneficial effects on reducing the `.mli` API.
---
 stm/vernac_classifier.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c93487d377..4db86817c9 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -189,7 +189,7 @@ let classify_vernac e =
     | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
-        try Vernacentries.get_vernac_classifier s l
+        try Vernacextend.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier = function
-- 
cgit v1.2.3