diff options
| author | Matthieu Sozeau | 2014-05-30 14:50:42 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-04 15:47:03 +0200 |
| commit | d2a025271724dac2cb129fa0f813a13a686c9972 (patch) | |
| tree | 939b901bd8eeda7c3f61928451cecf58cd1838dc | |
| parent | 848f2c41e605287c99e84c2f8ea1747c8a34e201 (diff) | |
- Keep all <= constraints during refinement, otherwise we might miss collapsed universes.
- Fix normalization with universe substitutions during refinement being inconsistent
with the one in the kernel.
| -rw-r--r-- | pretyping/evd.ml | 9 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 |
2 files changed, 3 insertions, 8 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index f5d1aa9f4c..42d98cdfef 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -369,7 +369,7 @@ let process_universe_constraints univs vars alg templ cstrs = if Univ.check_leq univs l r then (** Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) - if Univ.is_small_univ l then + if Univ.Universe.is_level l then match Univ.Universe.level r with | Some r -> Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local @@ -383,7 +383,7 @@ let process_universe_constraints univs vars alg templ cstrs = (if Univ.LSet.for_all (fun l -> Univ.Level.is_small l || Univ.LMap.mem l !vars) (Univ.Universe.levels l) then - Univ.enforce_eq l r local + Univ.enforce_leq l r local else raise (Univ.UniverseInconsistency (Univ.Le, l, r, []))) else if Univ.LSet.mem rl templ && Univ.Universe.is_level l then unify_universes fo l Univ.UEq r local @@ -1006,11 +1006,6 @@ let make_flexible_variable evd b u = {evd with universes = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'}} - -let instantiate_univ_variable evd v u = - let uvars' = Univ.LMap.add v (Some u) evd.universes.uctx_univ_variables in - {evd with universes = {evd.universes with uctx_univ_variables = uvars'}} - (****************************************) (* Operations on constants *) (****************************************) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 8e9deb6c06..150f1c2af6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1064,7 +1064,7 @@ let rec whd_evar sigma c = | None -> c) | Sort (Type u) -> let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Type u') + if u' == u then c else mkSort (Sorts.sort_of_univ u') | Const (c', u) when not (Univ.Instance.is_empty u) -> let u' = Evd.normalize_universe_instance sigma u in if u' == u then c else mkConstU (c', u') |