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.
---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 67a7e87d78..0e12b57b36 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -176,7 +176,7 @@ open Mltop
 open Record
 open Coqloop
 open Vernacentries
-open Vernacinterp
+open Vernacextend
 open Vernac
 
 (* Various utilities *)
-- 
cgit v1.2.3