From 3fb4d9dfc270aa7d4ea09fabbf857cfc11607019 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 7 Apr 2017 14:19:41 +0200
Subject: Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)

---
 dev/base_include    | 3 ---
 toplevel/coqinit.ml | 2 +-
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/dev/base_include b/dev/base_include
index 242405ae29..608624d06e 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -147,9 +147,6 @@ open Refiner
 open Tacmach
 open Tactic_debug
 
-open Decl_proof_instr
-open Decl_mode
-
 open Hints
 open Auto
 open Autorewrite
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 98f60924b9..ffd0d78051 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -127,7 +127,7 @@ let init_ocaml_path () =
       [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "engine" ]; [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
 	[ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ];
-        [ "grammar" ]; [ "ide" ]; [ "ltac" ]; ]
+        [ "grammar" ]; [ "ide" ]; [ "ltac" ]; [ "vernac" ]; ]
 
 let get_compat_version = function
   | "8.7" -> Flags.Current
-- 
cgit v1.2.3