aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include5
1 files changed, 4 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include
index f764eaf4f5..b30bbaa3fa 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -142,7 +142,6 @@ open Ind_tables
open Auto_ind_decl
open Coqinit
open Coqtop
-open Discharge
open Himsg
open Metasyntax
open Mltop
@@ -209,3 +208,7 @@ let _ =
print_string
("\n\tOcaml toplevel with Coq printers and utilities (use go();; to exit)\n\n");
flush_all()
+
+(* Local Variables: *)
+(* mode: tuareg *)
+(* End: *)