diff options
| author | Théo Zimmermann | 2019-02-22 19:06:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-22 19:06:57 +0100 |
| commit | 6a289e4fbc1c4327429bb7041e8f39a18bbb0f70 (patch) | |
| tree | 71d1b19fa90c0c2c6e398e386f162b940e46afc3 /dev/base_include | |
| parent | 237050870a27bc2eda9224e9d8b18b7ef5b66236 (diff) | |
| parent | fad095ccc656c5fccc5e50b36067deabde233bb3 (diff) | |
Merge PR #9561: [dev] Add include versions for Dune builds.
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 25 |
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 |