aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
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 /checker
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 'checker')
-rw-r--r--checker/inductive.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 1271a02b0..22353ec16 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1070,8 +1070,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) =
done
(*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
*)
(************************************************************************)