aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-02-12 04:32:47 +0100
committerEmilio Jesus Gallego Arias2019-02-18 18:15:44 +0100
commitfad095ccc656c5fccc5e50b36067deabde233bb3 (patch)
tree69374b6bea33db0cca8a5ea608aa7be3275fb559 /dev/base_include
parent77b454e5ab8698f0d87bdf2eb32b48ab998ba590 (diff)
[dev] Add include versions for Dune builds.
Fixes #9537 This way, users can do: ``` dune exec coqtop.byte > Drop. # #directory "dev";; # #use "include_dune";; ```
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include25
1 files changed, 0 insertions, 25 deletions
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