Cleanup "lbound" arguments which are always Set

engine/evd.ml

@@ -1063,8 +1063,8 @@ let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
   let uctx = UState.restrict uctx vars in
   ignore (UState.check_univ_decl ~poly uctx udecl)
 
-let restrict_universe_context ?lbound evd vars =
-  { evd with universes = UState.restrict ?lbound evd.universes vars }
+let restrict_universe_context evd vars =
+  { evd with universes = UState.restrict evd.universes vars }
 
 let universe_subst evd =
   UState.subst evd.universes

engine/evd.mli

@@ -535,7 +535,7 @@ val univ_flexible_alg : rigid
 
 type 'a in_ustate = 'a * UState.t
 
-val restrict_universe_context : ?lbound:UGraph.Bound.t -> evar_map -> Univ.Level.Set.t -> evar_map
+val restrict_universe_context : evar_map -> Univ.Level.Set.t -> evar_map
 
 (** Raises Not_found if not a name for a universe in this map. *)
 val universe_of_name : evar_map -> Id.t -> Univ.Level.t

engine/uState.ml

@@ -238,7 +238,7 @@ let empty =
     initial_universes = UGraph.initial_universes;
     minim_extra = UnivMinim.empty_extra; }
 
-let make ~lbound univs =
+let make univs =
   { empty with
     universes = univs;
     initial_universes = univs }
@@ -944,33 +944,30 @@ let check_univ_decl ~poly uctx decl =
     else Monomorphic_entry (check_mono_univ_decl uctx decl) in
   entry, binders
 
-let is_bound l lbound = match lbound with
-  | UGraph.Bound.Prop -> false
-  | UGraph.Bound.Set -> Level.is_set l
-
-let restrict_universe_context ?(lbound = UGraph.Bound.Set) (univs, csts) keep =
+let restrict_universe_context (univs, csts) keep =
   let removed = Level.Set.diff univs keep in
   if Level.Set.is_empty removed then univs, csts
   else
   let allunivs = Constraints.fold (fun (u,_,v) all -> Level.Set.add u (Level.Set.add v all)) csts univs in
   let g = UGraph.initial_universes in
-  let g = Level.Set.fold (fun v g -> if Level.is_set v then g else
-                        UGraph.add_universe v ~lbound ~strict:false g) allunivs g in
+  let g = Level.Set.fold (fun v g ->
+      if Level.is_set v then g else
+        UGraph.add_universe v ~lbound:Set ~strict:false g) allunivs g in
   let g = UGraph.merge_constraints csts g in
   let allkept = Level.Set.union (UGraph.domain UGraph.initial_universes) (Level.Set.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
-  let csts = Constraints.filter (fun (l,d,r) -> not (is_bound l lbound && d == Le)) csts in
+  let csts = Constraints.filter (fun (l,d,r) -> not (Level.is_set l && d == Le)) csts in
   (Level.Set.inter univs keep, csts)
 
-let restrict ?lbound uctx vars =
+let restrict uctx vars =
   let vars = Id.Map.fold (fun na l vars -> Level.Set.add l vars)
       (snd (fst uctx.names)) vars
   in
-  let uctx' = restrict_universe_context ?lbound uctx.local vars in
+  let uctx' = restrict_universe_context uctx.local vars in
   { uctx with local = uctx' }
 
-let restrict_even_binders ?lbound uctx vars =
-  let uctx' = restrict_universe_context ?lbound uctx.local vars in
+let restrict_even_binders uctx vars =
+  let uctx' = restrict_universe_context uctx.local vars in
   { uctx with local = uctx' }
 
 let restrict_constraints uctx csts =
@@ -1159,15 +1156,15 @@ let new_univ_variable ?loc rigid name uctx =
 
 let add_forgotten_univ uctx u = add_universe None true uctx u
 
-let make_with_initial_binders ~lbound univs binders =
-  let uctx = make ~lbound univs in
+let make_with_initial_binders univs binders =
+  let uctx = make univs in
   List.fold_left
     (fun uctx { CAst.loc; v = id } ->
        fst (new_univ_variable ?loc univ_rigid (Some id) uctx))
     uctx binders
 
 let from_env ?(binders=[]) env =
-  make_with_initial_binders ~lbound:UGraph.Bound.Set (Environ.universes env) binders
+  make_with_initial_binders (Environ.universes env) binders
 
 let make_nonalgebraic_variable uctx u =
   { uctx with univ_variables = UnivFlex.make_nonalgebraic_variable uctx.univ_variables u }
@@ -1198,10 +1195,10 @@ let collapse_above_prop_sort_variables ~to_prop uctx =
 let collapse_sort_variables uctx =
   { uctx with sort_variables = QState.collapse uctx.sort_variables }
 
-let minimize ?(lbound = UGraph.Bound.Set) uctx =
+let minimize uctx =
   let open UnivMinim in
   let (vars', us') =
-    normalize_context_set ~lbound uctx.universes uctx.local uctx.univ_variables
+    normalize_context_set uctx.universes uctx.local uctx.univ_variables
       uctx.minim_extra
   in
   if ContextSet.equal us' uctx.local then uctx

engine/uState.mli

@@ -32,10 +32,10 @@ type t
 
 val empty : t
 
-val make : lbound:UGraph.Bound.t -> UGraph.t -> t
+val make : UGraph.t -> t
 [@@ocaml.deprecated "(8.13) Use from_env"]
 
-val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
 [@@ocaml.deprecated "(8.13) Use from_env"]
 
 val from_env : ?binders:lident list -> Environ.env -> t
@@ -143,24 +143,24 @@ val name_level : Univ.Level.t -> Id.t -> t -> t
 
 (** {5 Unification} *)
 
-(** [restrict_universe_context lbound (univs,csts) keep] restricts [univs] to
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : ?lbound:UGraph.Bound.t -> ContextSet.t -> Level.Set.t -> ContextSet.t
+val restrict_universe_context : ContextSet.t -> Level.Set.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
    (from [demote_seff_univs]). Transitive constraints between retained
    universes are preserved. *)
-val restrict : ?lbound:UGraph.Bound.t -> t -> Univ.Level.Set.t -> t
+val restrict : t -> Univ.Level.Set.t -> t
 
 
 (** [restrict_even_binders uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by side effect universes
    (from [demote_seff_univs]). Transitive constraints between retained
    universes are preserved. *)
-val restrict_even_binders : ?lbound:UGraph.Bound.t -> t -> Univ.Level.Set.t -> t
+val restrict_even_binders : t -> Univ.Level.Set.t -> t
 
 type rigid =
   | UnivRigid
@@ -222,7 +222,7 @@ val fix_undefined_variables : t -> t
 (** cf UnivFlex *)
 
 (** Universe minimization *)
-val minimize : ?lbound:UGraph.Bound.t -> t -> t
+val minimize : t -> t
 
 val collapse_above_prop_sort_variables : to_prop:bool -> t -> t
 

engine/univMinim.ml

@@ -306,7 +306,7 @@ let extra_union a b = {
   above_prop = Level.Set.union a.above_prop b.above_prop;
 }
 
-let normalize_context_set ~lbound g ctx (us:UnivFlex.t) {weak_constraints=weak;above_prop} =
+let normalize_context_set g ctx (us:UnivFlex.t) {weak_constraints=weak;above_prop} =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Set <= i constraints separate *)
   let smallles, csts =
@@ -338,11 +338,9 @@ let normalize_context_set ~lbound g ctx (us:UnivFlex.t) {weak_constraints=weak;a
         else acc)
       weak (smallles, csts, g)
   in
-  let smallles = match (lbound : UGraph.Bound.t) with
-    | Prop -> smallles
-    | Set when get_set_minimization () ->
+  let smallles = if get_set_minimization () then
       Constraints.filter (fun (l,d,r) -> UnivFlex.mem r us) smallles
-    | Set -> Constraints.empty (* constraints Set <= u may be dropped *)
+    else  Constraints.empty (* constraints Set <= u may be dropped *)
   in
   let smallles = if get_set_minimization() then
       let fold u accu = if UnivFlex.mem u us then Constraints.add (Level.set, Le, u) accu else accu in

engine/univMinim.mli

@@ -33,7 +33,7 @@ val extra_union : extra -> extra -> extra
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t ->
+val normalize_context_set : UGraph.t -> ContextSet.t ->
   UnivFlex.t (* The defined and undefined variables *) ->
   extra ->
   UnivFlex.t in_universe_context_set