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/indschemes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/indschemes.ml')

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index facebd096..90168843a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -108,7 +108,7 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
-  let _, univs = Evd.universe_context ctx in
+  let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in
   let univs =
     if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
     else Monomorphic_const_entry univs
-- 
cgit v1.2.3