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/evd.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/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 21a0603c3f..52e37e611b 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -328,7 +328,7 @@ let diff_evar_universe_context ctx' ctx = uctx_universes = Univ.empty_universes } (* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *) -(* let diff_evar_universe_context = *) +(* let diff_evar_universe_context = *) (* Profile.profile2 diff_evar_universe_context_key diff_evar_universe_context;; *) type 'a in_evar_universe_context = 'a * evar_universe_context @@ -360,8 +360,9 @@ let process_universe_constraints univs postponed vars alg local cstrs = in if d == Univ.ULe then if Univ.check_leq univs l r then - (** Keep Prop <= var around if var might be instantiated by prop later. *) - if Univ.is_type0m_univ l && not (Univ.is_small_univ r) then + (** Keep Prop/Set <= var around if var might be instantiated by prop or set + later. *) + if Univ.is_small_univ l && not (Univ.is_small_univ r) then match Univ.Universe.level l, Univ.Universe.level r with | Some l, Some r -> Univ.Constraint.add (l,Univ.Le,r) local, postponed | _, _ -> local, postponed @@ -899,6 +900,9 @@ let merge orig ext = universes; metas = merge_metas orig.metas ext.metas } +(* let merge_key = Profile.declare_profile "merge" *) +(* let merge = Profile.profile2 merge_key merge *) + (**********************************************************) (* Sort variables *) @@ -1243,8 +1247,11 @@ let nf_constraints evd = let uctx' = normalize_evar_universe_context uctx' in {evd with universes = uctx'} -(* let nfconstrkey = Profile.declare_profile "nf_constraints";; *) -(* let nf_constraints = Profile.profile1 nfconstrkey nf_constraints;; *) +let nf_constraints = + if Flags.profile then + let nfconstrkey = Profile.declare_profile "nf_constraints" in + Profile.profile1 nfconstrkey nf_constraints + else nf_constraints let universes evd = evd.universes.uctx_universes |