From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 22:21:46 +0200
Subject: Stop exposing UState.universe_context and its Evd wrapper.

We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
---
 API/API.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 889050d90a..5c78606715 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2881,12 +2881,12 @@ 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 -> extensible:bool -> evar_map ->
-      Univ.UContext.t
     val universe_binders : evar_map -> Universes.universe_binders
     val nf_constraints : evar_map -> evar_map
     val from_ctx : UState.t -> evar_map
 
+    val to_universe_context : evar_map -> Univ.UContext.t
+
     val meta_list : evar_map -> (Constr.metavariable * clbinding) list
 
     val meta_defined : evar_map -> Constr.metavariable -> bool
-- 
cgit v1.2.3