diff options
| author | Matthieu Sozeau | 2013-11-14 11:50:04 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:55 +0200 |
| commit | c1cd47d5dff18f12af063d2c8defbd985c97dec6 (patch) | |
| tree | e459818ae127339883bb124a525191215a3b38f2 /pretyping/unification.ml | |
| parent | 28e5f4def8bebdaf3bd75b6662bbd4fd88594689 (diff) | |
- Fix comparison of universes.
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index dbd83bb42a..3bb3aa9baf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1370,12 +1370,15 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = | _ -> w_typed_unify env evd cv_pb flags ty1 ty2 (* Profiling *) -(* let wunifkey = Profile.declare_profile "w_unify";; *) -(* let w_unify env evd cv_pb flags ty1 ty2 = *) -(* w_unify env evd cv_pb ~flags: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 = Profile.profile6 wunifkey w_unify *) +let w_unify = + if Flags.profile then + let wunifkey = Profile.declare_profile "w_unify" in + Profile.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 *) +let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = + w_unify env evd cv_pb flags ty1 ty2 |