diff options
| author | Gaëtan Gilbert | 2019-01-24 13:18:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-24 13:18:28 +0100 |
| commit | ad227e6b900d15c60133e1997cdaed80358b85c7 (patch) | |
| tree | e17c2b2efc234c0bf49f11930c9d7e3a4004ad37 | |
| parent | f5241b99bb15f019eb629a7f24f2993f011e7e06 (diff) | |
Skip indirection through Evd for obligation ustate manipulation
| -rw-r--r-- | vernac/obligations.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6642d04c98..b4dd7d06b5 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -921,15 +921,15 @@ let obligation_hook prg obl num auto ctx' _ gr = | (true, Evar_kinds.Define true) -> if not transparent then err_not_transp () | _ -> () -in + in let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let inst, ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - let evd = Evd.from_env (Global.env ()) in - let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in - Univ.Instance.empty, Evd.evar_universe_context ctx' + let ctx = UState.make (Global.universes ()) in + let ctx' = UState.merge_subst ctx (UState.subst ctx') in + Univ.Instance.empty, ctx' else (* We get the right order somehow, but surely it could be enforced in a clearer way. *) let uctx = UState.context ctx' in |