diff options
| author | Matthieu Sozeau | 2019-02-05 14:35:35 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-05 14:35:35 +0100 |
| commit | 9d3394cbc37be3ad8b4fbd32d32c193a55368196 (patch) | |
| tree | 1e7e24ff7f862235e9daa45ea579191c1850d70b | |
| parent | 740ec848acc0b127fad7ba5b703bc00364126c71 (diff) | |
| parent | ad227e6b900d15c60133e1997cdaed80358b85c7 (diff) | |
Merge PR #9396: Skip indirection through Evd for obligation ustate manipulation
Reviewed-by: mattam82
| -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 |