From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 9 Sep 2017 14:00:42 +0200
Subject: Don't lose names in UState.universe_context.

We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
---
 vernac/obligations.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/obligations.ml')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c71feb52b..89b18d254 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -888,7 +888,7 @@ in
       let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
       Univ.Instance.empty, Evd.evar_universe_context ctx'
     else
-      let (_, uctx) = UState.universe_context ctx' in
+      let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in
       Univ.UContext.instance uctx, ctx'
   in
   let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
-- 
cgit v1.2.3