Remove Environ.set_universes / Typing.enrich_env

Made possible by the previous commit passing ~evars to
check_hyps_inclusion.

3 files changed, 0 insertions, 16 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f09f782008..cdb8836ed2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -350,9 +350,6 @@ let map_universes f env =
     { env with env_stratification =
 	 { s with env_universes = f s.env_universes } }
 
-let set_universes env u =
-  { env with env_stratification = { env.env_stratification with env_universes = u } }
-
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
   else map_universes (UGraph.merge_constraints c) env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 43bfe7c2fb..53a2eae7e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -155,11 +155,6 @@ val named_body : variable -> env -> constr option
 val fold_named_context :
   (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-val set_universes : env -> UGraph.t -> env
-(** This is used to update universes during a proof for the sake of
-   evar map-unaware functions, eg [Typing] calling
-   [Typeops.check_hyps_inclusion]. *)
-
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
   ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5a969eff6c..b5729d7574 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -218,9 +218,6 @@ let judge_of_cast env sigma cj k tj =
     sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
              uj_type = expected_type }
 
-let enrich_env env sigma =
-  set_universes env @@ Evd.universes sigma
-
 let check_fix env sigma pfix =
   let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   let (idx, (ids, cs, ts)) = pfix in
@@ -423,7 +420,6 @@ and execute_recdef env sigma (names,lar,vdef) =
 and execute_array env = Array.fold_left_map (execute env)
 
 let check env sigma c t =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   match Evarconv.cumul env sigma j.uj_type t with
   | None ->
@@ -433,14 +429,12 @@ let check env sigma c t =
 (* Type of a constr *)
 
 let unsafe_type_of env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   j.uj_type
 
 (* Sort of a type *)
 
 let sort_of env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   let sigma, a = type_judgment env sigma j in
   sigma, a.utj_type
@@ -448,7 +442,6 @@ let sort_of env sigma c =
 (* Try to solve the existential variables by typing *)
 
 let type_of ?(refresh=false) env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
     if refresh then
@@ -456,7 +449,6 @@ let type_of ?(refresh=false) env sigma c =
     else sigma, j.uj_type
 
 let solve_evars env sigma c =
-  let env = enrich_env env sigma in
   let sigma, j = execute env sigma c in
   (* side-effect on evdref *)
   sigma, nf_evar sigma j.uj_val