aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop_byte_bin.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-14 00:06:02 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-14 00:06:02 +0100
commit290abf59e6f13bb1468d8e3df050cf0bd9c48708 (patch)
treea61d3dce0bd34372b48668f44d280b5d886e2994 /toplevel/coqtop_byte_bin.ml
parent7576ffd4eb196d5d5a15f6cacb2ba5cba00576ef (diff)
parentf5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 (diff)
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Diffstat (limited to 'toplevel/coqtop_byte_bin.ml')
-rw-r--r--toplevel/coqtop_byte_bin.ml21
1 files changed, 21 insertions, 0 deletions
diff --git a/toplevel/coqtop_byte_bin.ml b/toplevel/coqtop_byte_bin.ml
new file mode 100644
index 000000000..7d8354ec3
--- /dev/null
+++ b/toplevel/coqtop_byte_bin.ml
@@ -0,0 +1,21 @@
+let drop_setup () =
+ begin try
+ (* Enable rectypes in the toplevel if it has the directive #rectypes *)
+ begin match Hashtbl.find Toploop.directive_table "rectypes" with
+ | Toploop.Directive_none f -> f ()
+ | _ -> ()
+ end
+ with
+ | Not_found -> ()
+ end;
+ let ppf = Format.std_formatter in
+ Mltop.(set_top
+ { load_obj = (fun f -> if not (Topdirs.load_file ppf f)
+ then CErrors.user_err Pp.(str ("Could not load plugin "^f))
+ );
+ use_file = Topdirs.dir_use ppf;
+ add_dir = Topdirs.dir_directory;
+ ml_loop = (fun () -> Toploop.loop ppf);
+ })
+
+let _ = drop_setup ()