aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refiner.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/refiner.ml')
-rw-r--r--proofs/refiner.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3e3313eb5..cd2b10906 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -30,8 +30,8 @@ let refiner pr goal_sigma =
(* Profiling refiner *)
let refiner =
if Flags.profile then
- let refiner_key = Profile.declare_profile "refiner" in
- Profile.profile2 refiner_key refiner
+ let refiner_key = CProfile.declare_profile "refiner" in
+ CProfile.profile2 refiner_key refiner
else refiner
(*********************)