Merge PR #7746: Many small cleanups removing unused arguments and functions

10 files changed, 20 insertions, 24 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 0c044f20d..b77bf55d8 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -495,12 +495,12 @@ let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid
     evdref := evd;
     c
 
-let new_Type ?(rigid=Evd.univ_flexible) env evd = 
+let new_Type ?(rigid=Evd.univ_flexible) evd =
   let open EConstr in
   let (evd, s) = new_sort_variable rigid evd in
   (evd, mkSort s)
 
-let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
+let e_new_Type ?(rigid=Evd.univ_flexible) evdref =
   let evd', s = new_sort_variable rigid !evdref in
     evdref := evd'; EConstr.mkSort s
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 135aa73fc..0ad323ac4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -63,7 +63,7 @@ val new_type_evar :
   env -> evar_map -> rigid ->
   evar_map * (constr * Sorts.t)
 
-val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
+val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
 
 (** Polymorphic constants *)
 
@@ -287,7 +287,7 @@ val e_new_type_evar : env -> evar_map ref ->
   ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
 [@@ocaml.deprecated "Use [Evarutil.new_type_evar]"]
 
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
+val e_new_Type : ?rigid:rigid -> evar_map ref -> constr
 [@@ocaml.deprecated "Use [Evarutil.new_Type]"]
 
 val e_new_global : evar_map ref -> GlobRef.t -> constr
diff --git a/engine/evd.ml b/engine/evd.ml
index 761ae7983..d1c7fef73 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -805,8 +805,8 @@ let make_flexible_variable evd ~algebraic u =
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
-  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
+  with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
 
 let fresh_constant_instance ?loc env evd c =
   with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
@@ -820,8 +820,6 @@ let fresh_constructor_instance ?loc env evd c =
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
   with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
 
-let whd_sort_variable evd t = t
-
 let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
 let is_flexible_level evd l = 
diff --git a/engine/evd.mli b/engine/evd.mli
index d638bb2d3..db2bd4eed 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -340,8 +340,6 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
     Evar maps also keep track of the universe constraints defined at a given
     point. This section defines the relevant manipulation functions. *)
 
-val whd_sort_variable : evar_map -> econstr -> econstr
-
 exception UniversesDiffer
 
 val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
@@ -598,7 +596,7 @@ val update_sigma_env : evar_map -> env -> evar_map
 
 (** Polymorphic universes *)
 
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t
 val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
 val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
diff --git a/engine/uState.ml b/engine/uState.ml
index 81ab3dd66..0791e4c27 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -583,7 +583,7 @@ let refresh_constraints univs (ctx, cstrs) =
   in ((ctx, cstrs'), univs')
 
 let normalize_variables uctx =
-  let normalized_variables, undef, def, subst = 
+  let normalized_variables, def, subst =
     UnivSubst.normalize_univ_variables uctx.uctx_univ_variables
   in
   let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 796a1bcc1..b07d4848f 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -215,7 +215,7 @@ let type_of_reference env r =
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
-let fresh_sort_in_family env = function
+let fresh_sort_in_family = function
   | InProp -> Sorts.prop, ContextSet.empty
   | InSet -> Sorts.set, ContextSet.empty
   | InType ->
@@ -223,7 +223,7 @@ let fresh_sort_in_family env = function
       Type (Univ.Universe.make u), ContextSet.singleton u
 
 let new_sort_in_family sf =
-  fst (fresh_sort_in_family (Global.env ()) sf)
+  fst (fresh_sort_in_family sf)
 
 let extend_context (a, ctx) (ctx') =
   (a, ContextSet.union ctx ctx')
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 8169dbda4..439424934 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -39,7 +39,7 @@ val fresh_instance_from_context : AUContext.t ->
 val fresh_instance_from : AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
 
-val fresh_sort_in_family : env -> Sorts.family ->
+val fresh_sort_in_family : Sorts.family ->
   Sorts.t in_universe_context_set
 val fresh_constant_instance : env -> Constant.t ->
   pconstant in_universe_context_set
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 6a433d9fb..2f59a3fa8 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -162,13 +162,13 @@ let subst_opt_univs_constr s =
 
 let normalize_univ_variables ctx =
   let ctx = normalize_opt_subst ctx in
-  let undef, def, subst =
-    Univ.LMap.fold (fun u v (undef, def, subst) ->
+  let def, subst =
+    Univ.LMap.fold (fun u v (def, subst) ->
       match v with
-      | None -> (Univ.LSet.add u undef, def, subst)
-      | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst))
-    ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty)
-  in ctx, undef, def, subst
+      | None -> (def, subst)
+      | Some b -> (Univ.LSet.add u def, Univ.LMap.add u b subst))
+    ctx (Univ.LSet.empty, Univ.LMap.empty)
+  in ctx, def, subst
 
 let pr_universe_body = function
   | None -> mt ()
diff --git a/engine/univSubst.mli b/engine/univSubst.mli
index 26e8d1db9..e76d25333 100644
--- a/engine/univSubst.mli
+++ b/engine/univSubst.mli
@@ -23,7 +23,7 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn
 val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 
 val normalize_univ_variables : universe_opt_subst ->
-  universe_opt_subst * LSet.t * LSet.t * universe_subst
+  universe_opt_subst * LSet.t * universe_subst
 
 val normalize_univ_variable :
   find:(Level.t -> Universe.t) ->
diff --git a/engine/universes.mli b/engine/universes.mli
index 29673de1e..ad937471e 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -86,7 +86,7 @@ val fresh_instance_from : AUContext.t -> Instance.t option ->
   Instance.t in_universe_context_set
 [@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"]
 
-val fresh_sort_in_family : env -> Sorts.family ->
+val fresh_sort_in_family : Sorts.family ->
   Sorts.t in_universe_context_set
 [@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"]
 
@@ -154,7 +154,7 @@ val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 [@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"]
 
 val normalize_univ_variables : universe_opt_subst ->
-  universe_opt_subst * LSet.t * LSet.t * universe_subst
+  universe_opt_subst * LSet.t * universe_subst
 [@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"]
 
 val normalize_univ_variable :