diff options
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 18db75eed5..43d562f77d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -2069,11 +2069,5 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = let w_unify env evd cv_pb flags ty1 ty2 = w_unify env evd cv_pb ~flags:flags ty1 ty2 -let w_unify = - if Flags.profile then - 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 = w_unify env evd cv_pb flags ty1 ty2 |