Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in naming

Ack-by: gares
Reviewed-by: ppedrot

21 files changed, 246 insertions, 244 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 4ae1d034d7..498a9d9825 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -832,9 +832,9 @@ let empty = {
   extras = Store.empty;
 }
 
-let from_env e = { empty with universes = UState.from_env e }
+let from_env ?binders e = { empty with universes = UState.from_env ?binders e }
 
-let from_ctx ctx = { empty with universes = ctx }
+let from_ctx uctx = { empty with universes = uctx }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
diff --git a/engine/evd.mli b/engine/evd.mli
index fafaad9a04..1c5c65924c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -153,12 +153,18 @@ type evar_map
 val empty : evar_map
 (** The empty evar map. *)
 
-val from_env : env -> evar_map
+val from_env : ?binders:lident list -> env -> evar_map
 (** The empty evar map with given universe context, taking its initial
-    universes from env. *)
+    universes from env, possibly with initial universe binders. This
+    is the main entry point at the beginning of the process of
+    interpreting a declaration (e.g. before entering the
+    interpretation of a Theorem statement). *)
 
 val from_ctx : UState.t -> evar_map
-(** The empty evar map with given universe context *)
+(** The empty evar map with given universe context. This is the main
+    entry point when resuming from a already interpreted declaration
+    (e.g.  after having interpreted a Theorem statement and preparing
+    to open a goal). *)
 
 val is_empty : evar_map -> bool
 (** Whether an evarmap is empty. *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 9557111cfd..103b552d86 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -25,8 +25,8 @@ module UPairSet = UnivMinim.UPairSet
 
 (* 2nd part used to check consistency on the fly. *)
 type t =
- { names : UnivNames.universe_binders * uinfo LMap.t;
-   local : ContextSet.t; (** The local context of variables *)
+ { names : UnivNames.universe_binders * uinfo LMap.t; (** Printing/location information *)
+   local : ContextSet.t; (** The local graph of universes (variables and constraints) *)
    seff_univs : LSet.t; (** Local universes used through private constants *)
    univ_variables : UnivSubst.universe_opt_subst;
    (** The local universes that are unification variables *)
@@ -56,18 +56,16 @@ let elaboration_sprop_cumul =
   Goptions.declare_bool_option_and_ref ~depr:false
     ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
 
-let make ~lbound u =
-  let u = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) u in
+let make ~lbound univs =
+  let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) univs in
   { empty with
-    universes = u;
+    universes = univs;
     universes_lbound = lbound;
-    initial_universes = u}
+    initial_universes = univs}
 
-let from_env e = make ~lbound:(Environ.universes_lbound e) (Environ.universes e)
-
-let is_empty ctx =
-  ContextSet.is_empty ctx.local &&
-    LMap.is_empty ctx.univ_variables
+let is_empty uctx =
+  ContextSet.is_empty uctx.local &&
+    LMap.is_empty uctx.univ_variables
 
 let uname_union s t =
   if s == t then s
@@ -77,42 +75,42 @@ let uname_union s t =
         | Some _, _ -> l
         | _, _ -> r) s t
 
-let union ctx ctx' =
-  if ctx == ctx' then ctx
-  else if is_empty ctx' then ctx
+let union uctx uctx' =
+  if uctx == uctx' then uctx
+  else if is_empty uctx' then uctx
   else
-    let local = ContextSet.union ctx.local ctx'.local in
-    let seff = LSet.union ctx.seff_univs ctx'.seff_univs in
-    let names = uname_union (fst ctx.names) (fst ctx'.names) in
-    let newus = LSet.diff (ContextSet.levels ctx'.local)
-                               (ContextSet.levels ctx.local) in
-    let newus = LSet.diff newus (LMap.domain ctx.univ_variables) in
-    let weak = UPairSet.union ctx.weak_constraints ctx'.weak_constraints in
+    let local = ContextSet.union uctx.local uctx'.local in
+    let seff = LSet.union uctx.seff_univs uctx'.seff_univs in
+    let names = uname_union (fst uctx.names) (fst uctx'.names) in
+    let names_rev = LMap.lunion (snd uctx.names) (snd uctx'.names) in
+    let newus = LSet.diff (ContextSet.levels uctx'.local)
+                               (ContextSet.levels uctx.local) in
+    let newus = LSet.diff newus (LMap.domain uctx.univ_variables) in
+    let weak = UPairSet.union uctx.weak_constraints uctx'.weak_constraints in
     let declarenew g =
-      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:ctx.universes_lbound ~strict:false g) newus g
+      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:uctx.universes_lbound ~strict:false g) newus g
     in
-    let names_rev = LMap.lunion (snd ctx.names) (snd ctx'.names) in
       { names = (names, names_rev);
         local = local;
         seff_univs = seff;
         univ_variables =
-          LMap.subst_union ctx.univ_variables ctx'.univ_variables;
+          LMap.subst_union uctx.univ_variables uctx'.univ_variables;
         univ_algebraic =
-          LSet.union ctx.univ_algebraic ctx'.univ_algebraic;
-        initial_universes = declarenew ctx.initial_universes;
+          LSet.union uctx.univ_algebraic uctx'.univ_algebraic;
+        initial_universes = declarenew uctx.initial_universes;
         universes =
-          (if local == ctx.local then ctx.universes
+          (if local == uctx.local then uctx.universes
            else
-             let cstrsr = ContextSet.constraints ctx'.local in
-             UGraph.merge_constraints cstrsr (declarenew ctx.universes));
-        universes_lbound = ctx.universes_lbound;
+             let cstrsr = ContextSet.constraints uctx'.local in
+             UGraph.merge_constraints cstrsr (declarenew uctx.universes));
+        universes_lbound = uctx.universes_lbound;
         weak_constraints = weak}
 
-let context_set ctx = ctx.local
+let context_set uctx = uctx.local
 
-let constraints ctx = snd ctx.local
+let constraints uctx = snd uctx.local
 
-let context ctx = ContextSet.to_context ctx.local
+let context uctx = ContextSet.to_context uctx.local
 
 let compute_instance_binders inst ubinders =
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
@@ -131,15 +129,15 @@ let univ_entry ~poly uctx =
     Polymorphic_entry (nas, uctx)
   else Monomorphic_entry (context_set uctx)
 
-let of_context_set ctx = { empty with local = ctx }
+let of_context_set local = { empty with local }
 
-let subst ctx = ctx.univ_variables
+let subst uctx = uctx.univ_variables
 
-let ugraph ctx = ctx.universes
+let ugraph uctx = uctx.universes
 
-let initial_graph ctx = ctx.initial_universes
+let initial_graph uctx = uctx.initial_universes
 
-let algebraics ctx = ctx.univ_algebraic
+let algebraics uctx = uctx.univ_algebraic
 
 let add_names ?loc s l (names, names_rev) =
   if UNameMap.mem s names
@@ -152,14 +150,13 @@ let add_loc l loc (names, names_rev) =
   | None -> (names, names_rev)
   | Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev)
 
-let of_binders b =
-  let ctx = empty in
-  let rmap =
+let of_binders names =
+  let rev_map =
     UNameMap.fold (fun id l rmap ->
         LMap.add l { uname = Some id; uloc = None } rmap)
-      b LMap.empty
+      names LMap.empty
   in
-  { ctx with names = b, rmap }
+  { empty with names = (names, rev_map) }
 
 let invent_name (named,cnt) u =
   let rec aux i =
@@ -169,14 +166,14 @@ let invent_name (named,cnt) u =
   in
   aux cnt
 
-let universe_binders ctx =
-  let named, rev = ctx.names in
+let universe_binders uctx =
+  let named, rev = uctx.names in
   let named, _ = LSet.fold (fun u named ->
       match LMap.find u rev with
       | exception Not_found -> (* not sure if possible *) invent_name named u
       | { uname = None } -> invent_name named u
       | { uname = Some _ } -> named)
-      (ContextSet.levels ctx.local) (named, 0)
+      (ContextSet.levels uctx.local) (named, 0)
   in
   named
 
@@ -192,12 +189,12 @@ let drop_weak_constraints =
     ~key:["Cumulativity";"Weak";"Constraints"]
     ~value:false
 
-let process_universe_constraints ctx cstrs =
+let process_universe_constraints uctx cstrs =
   let open UnivSubst in
   let open UnivProblem in
-  let univs = ctx.universes in
-  let vars = ref ctx.univ_variables in
-  let weak = ref ctx.weak_constraints in
+  let univs = uctx.universes in
+  let vars = ref uctx.univ_variables in
+  let weak = ref uctx.weak_constraints in
   let normalize u = normalize_univ_variable_opt_subst !vars u in
   let nf_constraint = function
     | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
@@ -231,7 +228,7 @@ let process_universe_constraints ctx cstrs =
   let equalize_universes l r local = match varinfo l, varinfo r with
   | Inr l', Inr r' -> equalize_variables false l l' r r' local
   | Inr l, Inl r | Inl r, Inr l ->
-    let alg = LSet.mem l ctx.univ_algebraic in
+    let alg = LSet.mem l uctx.univ_algebraic in
     let inst = univ_level_rem l r r in
       if alg && not (LSet.mem l (Universe.levels inst)) then
         (instantiate_variable l inst vars; local)
@@ -295,8 +292,8 @@ let process_universe_constraints ctx cstrs =
   in
     !vars, !weak, local
 
-let add_constraints ctx cstrs =
-  let univs, local = ctx.local in
+let add_constraints uctx cstrs =
+  let univs, old_cstrs = uctx.local in
   let cstrs' = Constraint.fold (fun (l,d,r) acc ->
     let l = Universe.make l and r = Universe.make r in
     let cstr' = let open UnivProblem in
@@ -308,27 +305,27 @@ let add_constraints ctx cstrs =
     in UnivProblem.Set.add cstr' acc)
     cstrs UnivProblem.Set.empty
   in
-  let vars, weak, local' = process_universe_constraints ctx cstrs' in
-  { ctx with
-    local = (univs, Constraint.union local local');
+  let vars, weak, cstrs' = process_universe_constraints uctx cstrs' in
+  { uctx with
+    local = (univs, Constraint.union old_cstrs cstrs');
     univ_variables = vars;
-    universes = UGraph.merge_constraints local' ctx.universes;
+    universes = UGraph.merge_constraints cstrs' uctx.universes;
     weak_constraints = weak; }
 
 (* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
 
-let add_universe_constraints ctx cstrs =
-  let univs, local = ctx.local in
-  let vars, weak, local' = process_universe_constraints ctx cstrs in
-  { ctx with
+let add_universe_constraints uctx cstrs =
+  let univs, local = uctx.local in
+  let vars, weak, local' = process_universe_constraints uctx cstrs in
+  { uctx with
     local = (univs, Constraint.union local local');
     univ_variables = vars;
-    universes = UGraph.merge_constraints local' ctx.universes;
+    universes = UGraph.merge_constraints local' uctx.universes;
     weak_constraints = weak; }
 
-let constrain_variables diff ctx =
-  let univs, local = ctx.local in
+let constrain_variables diff uctx =
+  let univs, local = uctx.local in
   let univs, vars, local =
     LSet.fold
       (fun l (univs, vars, cstrs) ->
@@ -340,9 +337,9 @@ let constrain_variables diff ctx =
               Constraint.add (l, Eq, Option.get (Universe.level u)) cstrs)
           | None -> (univs, vars, cstrs)
         with Not_found | Option.IsNone -> (univs, vars, cstrs))
-      diff (univs, ctx.univ_variables, local)
+      diff (univs, uctx.univ_variables, local)
   in
-  { ctx with local = (univs, local); univ_variables = vars }
+  { uctx with local = (univs, local); univ_variables = vars }
 
 let qualid_of_level uctx =
   let map, map_rev = uctx.names in
@@ -403,8 +400,8 @@ let universe_context ~names ~extensible uctx =
     let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
     let inst = Array.append (Array.of_list newinst) left in
     let inst = Instance.of_array inst in
-    let ctx = UContext.make (inst, ContextSet.constraints uctx.local) in
-    ctx
+    let uctx = UContext.make (inst, ContextSet.constraints uctx.local) in
+    uctx
 
 let check_universe_context_set ~names ~extensible uctx =
   if extensible then ()
@@ -439,27 +436,24 @@ let check_mono_univ_decl uctx decl =
   uctx.local
 
 let check_univ_decl ~poly uctx decl =
-  let ctx =
-    let names = decl.univdecl_instance in
-    let extensible = decl.univdecl_extensible_instance in
-    if poly then
-      let (binders, _) = uctx.names in
-      let uctx = universe_context ~names ~extensible uctx in
-      let nas = compute_instance_binders (UContext.instance uctx) binders in
-      Entries.Polymorphic_entry (nas, uctx)
-    else
-      let () = check_universe_context_set ~names ~extensible uctx in
-      Entries.Monomorphic_entry uctx.local
-  in
   if not decl.univdecl_extensible_constraints then
     check_implication uctx
       decl.univdecl_constraints
       (ContextSet.constraints uctx.local);
-  ctx
+  let names = decl.univdecl_instance in
+  let extensible = decl.univdecl_extensible_instance in
+  if poly then
+    let (binders, _) = uctx.names in
+    let uctx = universe_context ~names ~extensible uctx in
+    let nas = compute_instance_binders (UContext.instance uctx) binders in
+    Entries.Polymorphic_entry (nas, uctx)
+  else
+    let () = check_universe_context_set ~names ~extensible uctx in
+    Entries.Monomorphic_entry uctx.local
 
 let is_bound l lbound = match lbound with
-| UGraph.Bound.Prop -> Level.is_prop l
-| UGraph.Bound.Set -> Level.is_set l
+  | UGraph.Bound.Prop -> Level.is_prop l
+  | UGraph.Bound.Set -> Level.is_set l
 
 let restrict_universe_context ~lbound (univs, csts) keep =
   let removed = LSet.diff univs keep in
@@ -476,13 +470,13 @@ let restrict_universe_context ~lbound (univs, csts) keep =
       not ((is_bound l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
-let restrict ctx vars =
-  let vars = LSet.union vars ctx.seff_univs in
+let restrict uctx vars =
+  let vars = LSet.union vars uctx.seff_univs in
   let vars = Names.Id.Map.fold (fun na l vars -> LSet.add l vars)
-      (fst ctx.names) vars
+      (fst uctx.names) vars
   in
-  let uctx' = restrict_universe_context ~lbound:ctx.universes_lbound ctx.local vars in
-  { ctx with local = uctx' }
+  let uctx' = restrict_universe_context ~lbound:uctx.universes_lbound uctx.local vars in
+  { uctx with local = uctx' }
 
 type rigid =
   | UnivRigid
@@ -498,8 +492,8 @@ let univ_flexible_alg = UnivFlexible true
     context we merge comes from a side effect that is already inlined
     or defined separately. In the later case, there is no extension,
     see [emit_side_effects] for example. *)
-let merge ?loc ~sideff rigid uctx ctx' =
-  let levels = ContextSet.levels ctx' in
+let merge ?loc ~sideff rigid uctx uctx' =
+  let levels = ContextSet.levels uctx' in
   let uctx =
     match rigid with
     | UnivRigid -> uctx
@@ -514,7 +508,7 @@ let merge ?loc ~sideff rigid uctx ctx' =
                     univ_algebraic = LSet.union uctx.univ_algebraic levels }
       else { uctx with univ_variables = uvars' }
   in
-  let local = ContextSet.append ctx' uctx.local in
+  let local = ContextSet.append uctx' uctx.local in
   let declare g =
     LSet.fold (fun u g ->
         try UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u g
@@ -534,7 +528,7 @@ let merge ?loc ~sideff rigid uctx ctx' =
   in
   let initial = declare uctx.initial_universes in
   let univs = declare uctx.universes in
-  let universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+  let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in
   { uctx with names; local; universes;
               initial_universes = initial }
 
@@ -553,19 +547,18 @@ let demote_global_univs env uctx =
     ContextSet.(of_set global_univs |> add_constraints global_constraints) in
   { uctx with local = ContextSet.diff uctx.local promoted_uctx }
 
-let merge_seff uctx ctx' =
-  let levels = ContextSet.levels ctx' in
+let merge_seff uctx uctx' =
+  let levels = ContextSet.levels uctx' in
   let declare g =
     LSet.fold (fun u g ->
         try UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u g
         with UGraph.AlreadyDeclared -> g)
       levels g
   in
-  let initial = declare uctx.initial_universes in
+  let initial_universes = declare uctx.initial_universes in
   let univs = declare uctx.universes in
-  let universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
-  { uctx with universes;
-              initial_universes = initial }
+  let universes = UGraph.merge_constraints (ContextSet.constraints uctx') univs in
+  { uctx with universes; initial_universes }
 
 let emit_side_effects eff u =
   let uctx = Safe_typing.universes_of_private eff in
@@ -581,60 +574,54 @@ let update_sigma_univs uctx ugraph =
   in
   merge_seff eunivs eunivs.local
 
-let new_univ_variable ?loc rigid name
-  ({ local = ctx; univ_variables = uvars; univ_algebraic = avars} as uctx) =
-  let u = UnivGen.fresh_level () in
-  let ctx' = ContextSet.add_universe u ctx in
-  let uctx', pred =
-    match rigid with
-    | UnivRigid -> uctx, true
-    | UnivFlexible b ->
-      let uvars' = LMap.add u None uvars in
-        if b then {uctx with univ_variables = uvars';
-          univ_algebraic = LSet.add u avars}, false
-        else {uctx with univ_variables = uvars'}, false
-  in
+let add_universe ?loc name strict lbound uctx u =
+  let initial_universes = UGraph.add_universe ~lbound ~strict u uctx.initial_universes in
+  let universes = UGraph.add_universe ~lbound ~strict u uctx.universes in
+  let local = ContextSet.add_universe u uctx.local in
   let names =
     match name with
     | Some n -> add_names ?loc n u uctx.names
     | None -> add_loc u loc uctx.names
   in
-  let initial =
-    UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false u uctx.initial_universes
+  { uctx with names; local; initial_universes; universes }
+
+let new_univ_variable ?loc rigid name uctx =
+  let u = UnivGen.fresh_level () in
+  let uctx =
+    match rigid with
+    | UnivRigid -> uctx
+    | UnivFlexible allow_alg ->
+      let univ_variables = LMap.add u None uctx.univ_variables in
+      if allow_alg
+      then
+        let univ_algebraic = LSet.add u uctx.univ_algebraic in
+        { uctx with univ_variables; univ_algebraic }
+      else
+        { uctx with univ_variables }
   in
-  let uctx' =
-    {uctx' with names = names; local = ctx';
-                universes = UGraph.add_universe ~lbound:uctx.universes_lbound ~strict:false
-                    u uctx.universes;
-                initial_universes = initial}
-  in uctx', u
-
-let make_with_initial_binders ~lbound e us =
-  let uctx = make ~lbound e in
+  let uctx = add_universe ?loc name false uctx.universes_lbound uctx u in
+  uctx, u
+
+let add_global_univ uctx u = add_universe None true UGraph.Bound.Set uctx u
+
+let make_with_initial_binders ~lbound univs us =
+  let uctx = make ~lbound univs in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
     uctx us
 
-let add_global_univ uctx u =
-  let initial =
-    UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.initial_universes
-  in
-  let univs =
-    UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.universes
-  in
-  { uctx with local = ContextSet.add_universe u uctx.local;
-                                     initial_universes = initial;
-                                     universes = univs }
+let from_env ?(binders=[]) env =
+  make_with_initial_binders ~lbound:(Environ.universes_lbound env) (Environ.universes env) binders
 
-let make_flexible_variable ctx ~algebraic u =
+let make_flexible_variable uctx ~algebraic u =
   let {local = cstrs; univ_variables = uvars;
-       univ_algebraic = avars; universes=g; } = ctx in
+       univ_algebraic = avars; universes=g; } = uctx in
   assert (try LMap.find u uvars == None with Not_found -> true);
   match UGraph.choose (fun v -> not (Level.equal u v) && (algebraic || not (LSet.mem v avars))) g u with
   | Some v ->
     let uvars' = LMap.add u (Some (Universe.make v)) uvars in
-    { ctx with univ_variables = uvars'; }
+    { uctx with univ_variables = uvars'; }
   | None ->
     let uvars' = LMap.add u None uvars in
     let avars' =
@@ -652,14 +639,13 @@ let make_flexible_variable ctx ~algebraic u =
         then LSet.add u avars else avars
       else avars
     in
-    {ctx with univ_variables = uvars';
-              univ_algebraic = avars'}
+    { uctx with univ_variables = uvars'; univ_algebraic = avars' }
 
-let make_nonalgebraic_variable ctx u =
-  { ctx with univ_algebraic = LSet.remove u ctx.univ_algebraic }
+let make_nonalgebraic_variable uctx u =
+  { uctx with univ_algebraic = LSet.remove u uctx.univ_algebraic }
 
-let make_flexible_nonalgebraic ctx =
-  {ctx with univ_algebraic = LSet.empty}
+let make_flexible_nonalgebraic uctx =
+  { uctx with univ_algebraic = LSet.empty }
 
 let is_sort_variable uctx s =
   match s with
@@ -671,8 +657,8 @@ let is_sort_variable uctx s =
     | None -> None)
   | _ -> None
 
-let subst_univs_context_with_def def usubst (ctx, cst) =
-  (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst)
+let subst_univs_context_with_def def usubst (uctx, cst) =
+  (LSet.diff uctx def, UnivSubst.subst_univs_constraints usubst cst)
 
 let is_trivial_leq (l,d,r) =
   Level.is_prop l && (d == Le || d == Lt) && Level.is_set r
@@ -696,9 +682,9 @@ let normalize_variables uctx =
   let normalized_variables, def, subst =
     UnivSubst.normalize_univ_variables uctx.univ_variables
   in
-  let ctx_local = subst_univs_context_with_def def (make_subst subst) uctx.local in
-  let ctx_local', univs = refresh_constraints uctx.initial_universes ctx_local in
-    subst, { uctx with local = ctx_local';
+  let uctx_local = subst_univs_context_with_def def (make_subst subst) uctx.local in
+  let uctx_local', univs = refresh_constraints uctx.initial_universes uctx_local in
+    subst, { uctx with local = uctx_local';
       univ_variables = normalized_variables;
       universes = univs }
 
diff --git a/engine/uState.mli b/engine/uState.mli
index 7fec03e3b2..bd3aac0d8b 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -23,25 +23,34 @@ type t
 
 (** {5 Constructors} *)
 
+(** Different ways to create a new universe state *)
+
 val empty : t
 
 val make : lbound:UGraph.Bound.t -> UGraph.t -> t
+[@@ocaml.deprecated "Use from_env"]
 
 val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
+[@@ocaml.deprecated "Use from_env"]
 
-val from_env : Environ.env -> t
-
-val is_empty : t -> bool
+val from_env : ?binders:lident list -> Environ.env -> t
+(** Main entry point at the beginning of a declaration declaring the
+    binding names as rigid universes. *)
 
-val union : t -> t -> t
+val of_binders : UnivNames.universe_binders -> t
+(** Main entry point when only names matter, e.g. for printing. *)
 
 val of_context_set : Univ.ContextSet.t -> t
+(** Main entry point when starting from the instance of a global
+    reference, e.g. when building a scheme. *)
 
-val of_binders : UnivNames.universe_binders -> t
+(** Misc *)
 
-val universe_binders : t -> UnivNames.universe_binders
+val is_empty : t -> bool
+
+val union : t -> t -> t
 
-(** {5 Projections} *)
+(** {5 Projections and other destructors} *)
 
 val context_set : t -> Univ.ContextSet.t
 (** The local context of the state, i.e. a set of bound variables together
@@ -69,6 +78,9 @@ val context : t -> Univ.UContext.t
 val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
+val universe_binders : t -> UnivNames.universe_binders
+(** Return names of universes, inventing names if needed *)
+
 (** {5 Constraints handling} *)
 
 val add_constraints : t -> Univ.Constraint.t -> t
@@ -115,7 +127,7 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t
 val demote_global_univs : Environ.env -> t -> t
 (** Removes from the uctx_local part of the UState the universes and constraints
     that are present in the universe graph in the input env (supposedly the
-    global ones *)
+    global ones) *)
 
 val demote_seff_univs : Univ.LSet.t -> t -> t
 (** Mark the universes as not local any more, because they have been
@@ -123,6 +135,11 @@ val demote_seff_univs : Univ.LSet.t -> t -> t
    emit_side_effects instead. *)
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
+(** Declare a new local universe; use rigid if a global or bound
+    universe; use flexible for a universe existential variable; use
+    univ_flexible_alg for a universe existential variable allowed to
+    be instantiated with an algebraic universe *)
+
 val add_global_univ : t -> Univ.Level.t -> t
 
 (** [make_flexible_variable g algebraic l]
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8cc63c5d03..efc2a35b65 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -614,37 +614,3 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
   | _ ->
      CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
                       (str "This expression should be coercible to a pattern.")) c
-
-(** Local universe and constraint declarations. *)
-
-let interp_univ_constraints env evd cstrs =
-  let interp (evd,cstrs) (u, d, u') =
-    let ul = Pretyping.interp_known_glob_level evd u in
-    let u'l = Pretyping.interp_known_glob_level evd u' in
-    let cstr = (ul,d,u'l) in
-    let cstrs' = Univ.Constraint.add cstr cstrs in
-    try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
-        evd, cstrs'
-    with Univ.UniverseInconsistency e as exn ->
-      let _, info = Exninfo.capture exn in
-      CErrors.user_err ~hdr:"interp_constraint" ~info
-        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
-  in
-  List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-
-let interp_univ_decl env decl =
-  let open UState in
-  let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env)
-                            (Environ.universes env) pl) in
-  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = pl;
-    univdecl_extensible_instance = decl.univdecl_extensible_instance;
-    univdecl_constraints = cstrs;
-    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
-  in evd, decl
-
-let interp_univ_decl_opt env l =
-  match l with
-  | None -> Evd.from_env env, UState.default_univ_decl
-  | Some decl -> interp_univ_decl env decl
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index edf52c93e8..dfa51918d1 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -123,10 +123,3 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -
 
 (** For cases pattern parsing errors *)
 val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
-
-(** Local universe and constraint declarations. *)
-val interp_univ_decl : Environ.env -> universe_decl_expr ->
-                       Evd.evar_map * UState.universe_decl
-
-val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
-                       Evd.evar_map * UState.universe_decl
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ecf2b951a2..06cf19b4f7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2620,3 +2620,37 @@ let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env
   let int_env,bl = intern_context env impl_env params in
   let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in
   sigma, (int_env, x)
+
+
+(** Local universe and constraint declarations. *)
+
+let interp_univ_constraints env evd cstrs =
+  let interp (evd,cstrs) (u, d, u') =
+    let ul = Pretyping.interp_known_glob_level evd u in
+    let u'l = Pretyping.interp_known_glob_level evd u' in
+    let cstr = (ul,d,u'l) in
+    let cstrs' = Univ.Constraint.add cstr cstrs in
+    try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+        evd, cstrs'
+    with Univ.UniverseInconsistency e as exn ->
+      let _, info = Exninfo.capture exn in
+      CErrors.user_err ~hdr:"interp_constraint" ~info
+        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
+  in
+  List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+  let open UState in
+  let binders : lident list = decl.univdecl_instance in
+  let evd = Evd.from_env ~binders env in
+  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+  let decl = { univdecl_instance = binders;
+    univdecl_extensible_instance = decl.univdecl_extensible_instance;
+    univdecl_constraints = cstrs;
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+  in evd, decl
+
+let interp_univ_decl_opt env l =
+  match l with
+  | None -> Evd.from_env env, UState.default_univ_decl
+  | Some decl -> interp_univ_decl env decl
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 11d756803f..9037ed5414 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -197,3 +197,10 @@ val get_asymmetric_patterns : unit -> bool
 val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
 (** Check that a list of record field definitions doesn't contain
     duplicates. *)
+
+(** Local universe and constraint declarations. *)
+val interp_univ_decl : Environ.env -> universe_decl_expr ->
+                       Evd.evar_map * UState.universe_decl
+
+val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
+                       Evd.evar_map * UState.universe_decl
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 50f90ebea7..5f17d3e284 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -106,7 +106,7 @@ let transl_with_decl env base kind = function
   | CWith_Module ({CAst.v=fqid},qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
   | CWith_Definition ({CAst.v=fqid},udecl,c) ->
-    let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+    let sigma, udecl = interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
     let poly = lookup_polymorphism env base kind fqid in
     begin match UState.check_univ_decl ~poly ectx udecl with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 06f7d92e62..b70ff20e32 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -139,7 +139,7 @@ let interp_known_universe_level_name evd qid =
     let qid = Nametab.locate_universe qid in
     Univ.Level.make qid
 
-let interp_universe_level_name ~anon_rigidity evd qid =
+let interp_universe_level_name evd qid =
   try evd, interp_known_universe_level_name evd qid
   with Not_found ->
     if Libnames.qualid_is_ident qid then (* Undeclared *)
@@ -162,21 +162,15 @@ let interp_universe_level_name ~anon_rigidity evd qid =
         with UGraph.AlreadyDeclared -> evd
       in evd, level
 
-let interp_universe_name ?loc evd l =
-  (* [univ_flexible_alg] can produce algebraic universes in terms *)
-  let anon_rigidity = univ_flexible in
-  let evd', l = interp_universe_level_name ~anon_rigidity evd l in
-  evd', l
-
-let interp_sort_name ?loc sigma = function
+let interp_sort_name sigma = function
   | GSProp -> sigma, Univ.Level.sprop
   | GProp -> sigma, Univ.Level.prop
   | GSet -> sigma, Univ.Level.set
-  | GType l -> interp_universe_name ?loc sigma l
+  | GType l -> interp_universe_level_name sigma l
 
 let interp_sort_info ?loc evd l =
     List.fold_left (fun (evd, u) (l,n) ->
-      let evd', u' = interp_sort_name ?loc evd l in
+      let evd', u' = interp_sort_name evd l in
       let u' = Univ.Universe.make u' in
       let u' = match n with
       | 0 -> u'
@@ -410,7 +404,7 @@ let interp_known_glob_level ?loc evd = function
 
 let interp_glob_level ?loc evd : glob_level -> _ = function
   | UAnonymous {rigid} -> new_univ_level_variable ?loc (if rigid then univ_rigid else univ_flexible) evd
-  | UNamed s -> interp_sort_name ?loc evd s
+  | UNamed s -> interp_sort_name evd s
 
 let interp_instance ?loc evd l =
   let evd, l' =
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 9164a4ff26..b16153a39e 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -100,9 +100,9 @@ let check_scheme kind ind = Option.has_some (lookup_scheme kind ind)
 
 let define internal role id c poly univs =
   let id = compute_name internal id in
-  let ctx = UState.minimize univs in
-  let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
-  let univs = UState.univ_entry ~poly ctx in
+  let uctx = UState.minimize univs in
+  let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst uctx) c in
+  let univs = UState.univ_entry ~poly uctx in
   !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
 (* Assumes that dependencies are already defined *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a100352145..054addc542 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -503,7 +503,7 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx'
     declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype
 
 let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
-  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
+  let sigma, decl = interp_univ_decl_opt env pl in
   let tclass =
     if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
     else tclass
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 12194ea20c..9e850ff1c7 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -13,7 +13,6 @@ open Util
 open Vars
 open Names
 open Context
-open Constrexpr_ops
 open Constrintern
 open Impargs
 open Pretyping
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 3fc74cba5b..81154bbea9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -114,7 +114,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct
   let program_mode = false in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
-  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+  let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
@@ -134,7 +134,7 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red
   let program_mode = true in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
-  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+  let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
     interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt
   in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 29bf5fbcc2..dd6c985bf9 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -176,7 +176,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
            if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
              CErrors.user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
            Some us) fixl None in
-  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env all_universes in
+  let sigma, decl = interp_univ_decl_opt env all_universes in
   let sigma, (fixctxs, fiximppairs, fixannots) =
     on_snd List.split3 @@
       List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index eaa5271a73..a910cc6e8b 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -30,7 +30,7 @@ let do_primitive id udecl prim typopt =
     declare id {Entries.prim_entry_type = None; prim_entry_content = prim}
   | Some typ ->
     let env = Global.env () in
-    let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+    let evd, udecl = Constrintern.interp_univ_decl_opt env udecl in
     let auctx = CPrimitives.op_or_type_univs prim in
     let evd, u = Evd.with_context_set UState.univ_flexible evd (UnivGen.fresh_instance auctx) in
     let expected_typ = EConstr.of_constr @@ Typeops.type_of_prim_or_type env u prim in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 9623317ddf..31f91979d3 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -115,7 +115,7 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notat
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
+  let sigma, udecl = interp_univ_decl_opt env pl in
   let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 367d0bf944..1e8771b641 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1291,7 +1291,7 @@ let obligation_terminator ~pm ~entry ~uctx ~oinfo:{name; num; auto} =
 
    FIXME: There is duplication of this code with obligation_terminator
    and Obligations.admit_obligations *)
-let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref =
+let obligation_admitted_terminator ~pm {name; num; auto} uctx' dref =
   let prg = Option.get (State.find pm name) in
   let {obls; remaining = rem} = prg.prg_obligations in
   let obl = obls.(num) in
@@ -1303,21 +1303,21 @@ let obligation_admitted_terminator ~pm {name; num; auto} ctx' dref =
       if not transparent then err_not_transp ()
     | _ -> ()
   in
-  let inst, ctx' =
+  let inst, uctx' =
     if not prg.prg_info.Info.poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
-      let ctx = UState.from_env (Global.env ()) in
-      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
-      (Univ.Instance.empty, ctx')
+      let uctx = UState.from_env (Global.env ()) in
+      let uctx' = UState.merge_subst uctx (UState.subst uctx') in
+      (Univ.Instance.empty, uctx')
     else
       (* 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')
+      let uctx = UState.context uctx' in
+      (Univ.UContext.instance uctx, uctx')
   in
   let obl = {obl with obl_body = Some (DefinedObl (cst, inst))} in
   let () = if transparent then add_hint true prg cst in
-  update_program_decl_on_defined ~pm prg obls num obl ~uctx:ctx' rem ~auto
+  update_program_decl_on_defined ~pm prg obls num obl ~uctx:uctx' rem ~auto
 
 end
 
@@ -1627,12 +1627,12 @@ let make_univs_deferred ~poly ~initial_euctx ~uctx ~udecl
 
 let make_univs_private_poly ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) =
   let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-  let universes = UState.restrict uctx used_univs in
-  let typus = UState.restrict universes used_univs_typ in
-  let utyp = UState.check_univ_decl ~poly typus udecl in
+  let uctx = UState.restrict uctx used_univs in
+  let uctx' = UState.restrict uctx used_univs_typ in
+  let utyp = UState.check_univ_decl ~poly uctx' udecl in
   let ubody = Univ.ContextSet.diff
-      (UState.context_set universes)
-      (UState.context_set typus)
+      (UState.context_set uctx)
+      (UState.context_set uctx')
   in
   utyp, ubody
 
@@ -1643,8 +1643,8 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body)
      for the typ. We recheck the declaration after restricting with
      the actually used universes.
      TODO: check if restrict is really necessary now. *)
-  let ctx = UState.restrict uctx used_univs in
-  let utyp = UState.check_univ_decl ~poly ctx udecl in
+  let uctx = UState.restrict uctx used_univs in
+  let utyp = UState.check_univ_decl ~poly uctx udecl in
   utyp, Univ.ContextSet.empty
 
 let close_proof ~opaque ~keep_body_ucst_separate ps =
@@ -1712,9 +1712,9 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
             (Vars.universes_of_constr types)
             (Vars.universes_of_constr pt)
         in
-        let univs = UState.restrict uctx used_univs in
-        let univs = UState.check_mono_univ_decl univs udecl in
-        (pt,univs),eff)
+        let uctx = UState.restrict uctx used_univs in
+        let uctx = UState.check_mono_univ_decl uctx udecl in
+        (pt,uctx),eff)
     |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types
   in
   let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 06f7c32cdc..840754ccc6 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -631,11 +631,11 @@ let print_constant with_values sep sp udecl =
         assert(ContextSet.is_empty body_uctxs);
         Polymorphic ctx
   in
-  let ctx =
+  let uctx =
     UState.of_binders
       (Printer.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl)
   in
-  let env = Global.env () and sigma = Evd.from_ctx ctx in
+  let env = Global.env () and sigma = Evd.from_ctx uctx in
   let pr_ltype = pr_ltype_env env sigma in
   hov 0 (
     match val_0 with
diff --git a/vernac/record.ml b/vernac/record.ml
index acc97f61c1..2c56604d8f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -124,7 +124,7 @@ let typecheck_params_and_fields def poly pl ps records =
   let is_template =
     List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
   let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
-  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
+  let sigma, decl = interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =
       match bk, name with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef8631fbb6..824bf35b1d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -550,7 +550,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
   let env0 = Global.env () in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
-  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
+  let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
   let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in