From fad095ccc656c5fccc5e50b36067deabde233bb3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 04:32:47 +0100
Subject: [dev] Add include versions for Dune builds.

Fixes #9537

This way, users can do:
```
dune exec coqtop.byte
> Drop.
 # #directory "dev";;
 # #use "include_dune";;
```
---
 dev/base_include | 25 -------------------------
 1 file changed, 25 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 48feeec147..b214959bad 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -1,24 +1,6 @@
-
 (* File to include to get some Coq facilities under the ocaml toplevel.
    This file is loaded by include *)
 
-#cd".";;
-#directory "parsing";;
-#directory "interp";;
-#directory "toplevel";;
-#directory "library";;
-#directory "kernel";;
-#directory "gramlib";;
-#directory "engine";;
-#directory "pretyping";;
-#directory "lib";;
-#directory "proofs";;
-#directory "tactics";;
-#directory "printing";;
-#directory "grammar";;
-#directory "stm";;
-#directory "vernac";;
-
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -137,7 +119,6 @@ open Proof_global
 open Redexpr
 open Refiner
 open Tacmach
-open Tactic_debug
 
 open Hints
 open Auto
@@ -146,15 +127,9 @@ open Contradiction
 open Eauto
 open Elim
 open Equality
-open Evar_tactics
-open Extraargs
-open Extratactics
 open Hipattern
 open Inv
 open Leminv
-open Tacsubst
-open Tacintern
-open Tacinterp
 open Tacticals
 open Tactics
 open Eqschemes
-- 
cgit v1.2.3