aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-05 12:34:36 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-09 19:01:46 +0100
commitd0f89f8c59cda2e7e74fec693e511e910fbc0434 (patch)
treed72a404ba6d47f7b29b80775c0731cd765d448dc /toplevel
parent319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 (diff)
[lib] Rename Profile to CProfile
New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 553da2dc0..b62396317 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,7 @@ 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 *)