From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
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.
---
 API/API.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 83f4a3c500..bb644c3886 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2308,7 +2308,7 @@ sig
     val universe_context_set : evar_map -> Univ.ContextSet.t
     val evar_ident : evar -> evar_map -> Names.Id.t option
     val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-    val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map ->
+    val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map ->
                            (Names.Id.t * Univ.Level.t) list * Univ.UContext.t
     val nf_constraints : evar_map -> evar_map
     val from_ctx : UState.t -> evar_map
-- 
cgit v1.2.3