diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-05-27 11:43:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-05-27 11:43:11 +0200 |
| commit | 866c41b9720413e00194ba7addb9c4277e114890 (patch) | |
| tree | 37fe660b28acfbaa6f3f304b6b9f3eebcf15dddb /pretyping | |
| parent | ec5ef15aae0d6f900eb4a8e6ba61c0952c993eb3 (diff) | |
Fix bug #4159
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 16 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 |
2 files changed, 16 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 18e668d28..fe96aa347 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -330,9 +330,23 @@ let union_evar_universe_context ctx ctx' = type 'a in_evar_universe_context = 'a * evar_universe_context -let evar_universe_context_set ctx = ctx.uctx_local +let evar_universe_context_set diff ctx = + let initctx = ctx.uctx_local in + let cstrs = + Univ.LSet.fold + (fun l cstrs -> + try + match Univ.LMap.find l ctx.uctx_univ_variables with + | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs + | None -> cstrs + with Not_found -> cstrs) + (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty + in + Univ.ContextSet.add_constraints cstrs initctx + let evar_universe_context_constraints ctx = snd ctx.uctx_local let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local + let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } let evar_universe_context_subst ctx = ctx.uctx_univ_variables diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 15ce979d0..f2d8a8335 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -475,7 +475,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * evar_universe_context -val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set +val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set val evar_universe_context_constraints : evar_universe_context -> Univ.constraints val evar_context_universe_context : evar_universe_context -> Univ.universe_context val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context |