diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1b1aa84e6b..3a946fc03a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -644,12 +644,6 @@ let infer env constr = let constr, t = execute env constr in make_judge constr t -let infer = - if Flags.profile then - let infer_key = CProfile.declare_profile "Fast_infer" in - CProfile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - let assumption_of_judgment env {uj_val=c; uj_type=t} = infer_assumption env c t |