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).
---
 plugins/funind/functional_principles_types.ml | 2 +-
 plugins/funind/recdef.ml                      | 2 +-
 plugins/ltac/rewrite.ml                       | 2 +-
 plugins/setoid_ring/newring.ml                | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d5bff57af0..076fba861d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -348,7 +348,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
         (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-        let univs = Evd.universe_context ~names:[] ~extensible:true evd' in
+        let univs = Evd.to_universe_context evd' in
         let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
 	ignore(
 	  Declare.declare_constant
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 63896bb560..320f7c7f31 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1556,7 +1556,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
-    let ctx = Evd.universe_context ~names:[] ~extensible:true evm in
+    let ctx = Evd.to_universe_context evm in
     declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
   in
   (* Refresh the global universes, now including those of _F *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2eb6602196..f6523d28c2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,7 +1884,7 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
+  let ctx = Evd.to_universe_context sigma in
   let typ = EConstr.to_constr sigma typ in
   let term = EConstr.to_constr sigma term in
   let cst = 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index a37b35b3d0..6d0b6fd09f 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
   let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
   let nf c = nf (constr_of c) in
-  Array.map nf !tactic_res, Evd.universe_context ~names:[] ~extensible:true evd
+  Array.map nf !tactic_res, Evd.to_universe_context evd
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
-- 
cgit v1.2.3