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

18 files changed, 47 insertions, 46 deletions

diff --git a/API/API.mli b/API/API.mli
index 889050d90..5c7860671 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
diff --git a/engine/evd.ml b/engine/evd.ml
index 67ae73ceb..eb0f2e3e7 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -756,8 +756,7 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let universe_context ~names ~extensible evd =
-  UState.universe_context ~names ~extensible evd.universes
+let to_universe_context evd = UState.context evd.universes
 
 let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
 
diff --git a/engine/evd.mli b/engine/evd.mli
index b6157202d..49b6a7583 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -492,6 +492,8 @@ type 'a in_evar_universe_context = 'a * UState.t
 val evar_universe_context_set : UState.t -> Univ.ContextSet.t
 val evar_universe_context_constraints : UState.t -> Univ.constraints
 val evar_context_universe_context : UState.t -> Univ.UContext.t
+[@@ocaml.deprecated "alias of UState.context"]
+
 val evar_universe_context_of : Univ.ContextSet.t -> UState.t
 val empty_evar_universe_context : UState.t
 val union_evar_universe_context : UState.t -> UState.t ->
@@ -552,11 +554,14 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
 
 val evar_universe_context : evar_map -> UState.t
 val universe_context_set : evar_map -> Univ.ContextSet.t
-val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map ->
-  Univ.UContext.t
 val universe_subst : evar_map -> Universes.universe_opt_subst
 val universes : evar_map -> UGraph.t
 
+(** [to_universe_context evm] extracts the local universes and
+    constraints of [evm] and orders the universes the same as
+    [Univ.ContextSet.to_context]. *)
+val to_universe_context : evar_map -> Univ.UContext.t
+
 val check_univ_decl : evar_map -> UState.universe_decl ->
   Univ.UContext.t
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 38af08f91..5279c6388 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -125,23 +125,18 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 val normalize : t -> t
 
-(** [universe_context names extensible ctx]
-
-    Return a universe context containing the local universes of [ctx]
-    and their constraints. The universes corresponding to [names] come
-    first in the order defined by that list.
-
-    If [extensible] is false, check that the universes of [names] are
-    the only local universes.
-
-    Also return the association list of universe names and universes
-    (including those not in [names]). *)
-val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t ->
-  Univ.UContext.t
-
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
+(** [check_univ_decl ctx decl]
+
+   If non extensible in [decl], check that the local universes (resp.
+   universe constraints) in [ctx] are implied by [decl].
+
+   Return a universe context containing the local universes of [ctx]
+   and their constraints. The universes corresponding to
+   [decl.univdecl_instance] come first in the order defined by that
+   list. *)
 val check_univ_decl : t -> universe_decl -> Univ.UContext.t
 
 (** {5 TODO: Document me} *)
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 08657936e..3eb91d8cd 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,7 +62,7 @@ let transl_with_decl env = function
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
     let c, ectx = interp_constr env (Evd.from_env env) c in
-    let ctx = Evd.evar_context_universe_context ectx in
+    let ctx = UState.context ectx in
       WithDef (fqid,(c,ctx))
 
 let loc_of_module l = l.CAst.loc
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d5bff57af..076fba861 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 63896bb56..320f7c7f3 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 2eb660219..f6523d28c 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 a37b35b3d..6d0b6fd09 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"];
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9faff3211..ea0408169 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
         let used_univs_typ = Univops.universes_of_constr typ in
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
-          let initunivs = Evd.evar_context_universe_context initial_euctx in
+          let initunivs = UState.context initial_euctx in
           let ctx = constrain_variables initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e7fa555c2..92c326b1e 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,7 +123,7 @@ let define internal id c p univs =
   let ctx = Evd.normalize_evar_universe_context univs in
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
-  let univs = Evd.evar_context_universe_context ctx in
+  let univs = UState.context ctx in
   let univs =
     if p then Polymorphic_const_entry univs
     else Monomorphic_const_entry univs
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4d1b271d6..1ee873e0f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
   let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
-    p, Evd.universe_context ~names:[] ~extensible:true sigma
+    p, Evd.to_universe_context sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 7eaafc354..00cab744e 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -190,6 +190,8 @@ Module binders.
     Fail Defined.
   Abort.
 
+  Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat.
+
   Lemma bar@{i j| i < j} : Type@{j}.
   Proof.
     exact Type@{i}.
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