From ad227e6b900d15c60133e1997cdaed80358b85c7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 24 Jan 2019 13:18:28 +0100
Subject: Skip indirection through Evd for obligation ustate manipulation

---
 vernac/obligations.ml | 8 ++++----
 1 file 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
-- 
cgit v1.2.3