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).

5 files changed, 18 insertions, 18 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index e59482b71..68fd22cb6 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly =
 	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
-  let univs = Evd.universe_context ~names:[] ~extensible:true sigma in
+  let univs = Evd.to_universe_context sigma in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
       (definition_entry ~types:typ_f ~poly ~univs
diff --git a/vernac/command.ml b/vernac/command.ml
index 5a063f173..80599c534 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1022,8 +1022,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders_rel = nf_evar_context !evdref binders_rel in
   let binders = nf_evar_context !evdref binders in
   let top_arity = Evarutil.nf_evar !evdref top_arity in
-  let pl, plext = Option.cata
-      (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
   let hook, recname, typ =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
@@ -1031,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
         let ty = EConstr.Unsafe.to_constr ty in
-        let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
+        let univs = Evd.check_univ_decl !evdref decl in
         (*FIXME poly? *)
         let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
         (** FIXME: include locality *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 58f39e303..c728c2671 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,7 +109,7 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
-  let univs = Evd.universe_context ~names:[] ~extensible:true ctx in
+  let univs = Evd.to_universe_context ctx in
   let univs =
     if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
     else Monomorphic_const_entry univs
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index cd30c7a68..71d80c4db 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,8 @@ let retrieve_first_recthm uctx = function
       (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      let uctx = UState.universe_context ~names:[] ~extensible:true uctx in
+      (* we get the right order somehow but surely it could be enforced in a better way *)
+      let uctx = UState.context uctx in
       let inst = Univ.UContext.instance uctx in
       let map (c, ctx) = Vars.subst_instance_constr inst c in
       (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -420,8 +421,8 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-            let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
-	    let body = Option.map norm body in
+            let ctx = UState.check_univ_decl ctx decl in
+            let body = Option.map norm body in
             List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
@@ -453,9 +454,9 @@ let start_proof_com ?inference_hook kind thms hook =
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
   let () =
-    if not decl.Misctypes.univdecl_extensible_instance then
-       ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
-    else ()
+    let open Misctypes in
+    if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
+       ignore (Evd.check_univ_decl evd decl)
   in
   let evd =
     if pi2 kind then evd
@@ -490,7 +491,7 @@ let save_proof ?proof = function
             if const_entry_type = None then
               user_err Pp.(str "Admitted requires an explicit statement");
             let typ = Option.get const_entry_type in
-            let ctx = Evd.evar_context_universe_context (fst universes) in
+            let ctx = UState.context (fst universes) in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
         | None ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 216801811..43af8968f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -479,7 +479,7 @@ let declare_definition prg =
   let ce =
     definition_entry ~fix_exn
      ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
+     ~univs:(UState.context prg.prg_ctx) (nf body)
   in
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders prg.prg_ctx in
@@ -549,7 +549,7 @@ let declare_mutual_definition l =
             mk_proof (mkCoFix (i,fixdecls))) 0 l
   in
   (* Declare the recursive definitions *)
-  let ctx = Evd.evar_context_universe_context first.prg_ctx in
+  let ctx = UState.context first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
   let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx)
     fixnames fixdecls fixtypes fiximps in
@@ -855,7 +855,7 @@ let obligation_terminator name num guard hook auto pf =
         | (_, status), Vernacexpr.Transparent -> status
       in
       let obl = { obl with obl_status = false, status } in
-      let uctx = Evd.evar_context_universe_context ctx in
+      let uctx = UState.context ctx in
       let (_, obl) = declare_obligation prg obl body ty uctx in
       let obls = Array.copy obls in
       let _ = obls.(num) <- obl in
@@ -890,7 +890,8 @@ 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 ~names:[] ~extensible:true ctx' in
+      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+      let uctx = UState.context ctx' in
       Univ.UContext.instance uctx, ctx'
   in
   let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
@@ -969,7 +970,7 @@ and solve_obligation_by_tac prg obls i tac =
 	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
 	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
 	    in
-	    let uctx = Evd.evar_context_universe_context ctx in
+            let uctx = UState.context ctx in
 	    let prg = {prg with prg_ctx = ctx} in
 	    let def, obl' = declare_obligation prg obl t ty uctx in
 	      obls.(i) <- obl';
@@ -1120,7 +1121,7 @@ let admit_prog prg =
         match x.obl_body with
         | None ->
             let x = subst_deps_obl obls x in
-	    let ctx = Evd.evar_context_universe_context prg.prg_ctx in
+            let ctx = UState.context prg.prg_ctx in
             let kn = Declare.declare_constant x.obl_name ~local:true
               (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in