aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
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 /pretyping/unification.ml
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 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 84ffab426..08329391d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 =
let w_unify =
if Flags.profile then
- let wunifkey = Profile.declare_profile "w_unify" in
- Profile.profile6 wunifkey w_unify
+ let wunifkey = CProfile.declare_profile "w_unify" in
+ CProfile.profile6 wunifkey w_unify
else w_unify
let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =