diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 663e24f9f..da9e8c68d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -28,8 +28,11 @@ let refiner pr goal_sigma = { it = sgl; sigma = sigma'; } (* Profiling refiner *) -(* let refiner_key = Profile.declare_profile "refiner" *) -(* let refiner = Profile.profile2 refiner_key refiner *) +let refiner = + if Flags.profile then + let refiner_key = Profile.declare_profile "refiner" in + Profile.profile2 refiner_key refiner + else refiner (*********************) (* Tacticals *) |