diff options
Diffstat (limited to 'kernel/fast_typeops.ml')
| -rw-r--r-- | kernel/fast_typeops.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index e03720997c..bb56958851 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -478,8 +478,11 @@ let infer env constr = let t = execute env constr in make_judge constr t -(* let infer_key = Profile.declare_profile "Fast_infer" *) -(* let infer = Profile.profile2 infer_key infer *) +let infer = + if Flags.profile then + let infer_key = Profile.declare_profile "Fast_infer" in + Profile.profile2 infer_key infer + else infer let infer_type env constr = execute_type env constr |