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 ---
 1 file changed, 3 deletions(-)

(limited to 'dev/base_include')

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
-- 
cgit v1.2.3