aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.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.ml
parent7576ffd4eb196d5d5a15f6cacb2ba5cba00576ef (diff)
parentf5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 (diff)
Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml6
1 files changed, 2 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 *)