Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.

4 files changed, 28 insertions, 4 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6048dae3b..2fa9f0ab4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -756,7 +756,7 @@ let init_toplevel arglist =
   (* Coq's init process, phase 1:
      - OCaml parameters, and basic structures and IO
    *)
-  Profile.init_profile ();
+  CProfile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in
@@ -846,7 +846,5 @@ let start () =
       let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
     end;
-    Profile.print_profile ();
+    CProfile.print_profile ();
     exit 0
-
-(* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/coqtop_bin.ml b/toplevel/coqtop_bin.ml
new file mode 100644
index 000000000..56aced92a
--- /dev/null
+++ b/toplevel/coqtop_bin.ml
@@ -0,0 +1,2 @@
+(* Main coqtop initialization *)
+let () = Coqtop.start()
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 ()
diff --git a/toplevel/coqtop_opt_bin.ml b/toplevel/coqtop_opt_bin.ml
new file mode 100644
index 000000000..410b4679a
--- /dev/null
+++ b/toplevel/coqtop_opt_bin.ml
@@ -0,0 +1,3 @@
+let drop_setup () = Mltop.remove ()
+
+let _ = drop_setup ()