Removing dead code from Evd.

2 files changed, 0 insertions, 29 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e1d5c5a985..a3c9e39636 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -16,7 +16,6 @@ open Vars
 open Termops
 open Environ
 open Globnames
-open Mod_subst
 
 (** Generic filters *)
 module Filter :
@@ -730,29 +729,6 @@ let is_empty d =
   List.is_empty d.conv_pbs &&
   Metamap.is_empty d.metas
 
-let subst_named_context_val s = map_named_val (subst_mps s)
-
-let subst_evar_info s evi =
-  let subst_evb = function
-  | Evar_empty -> Evar_empty
-  | Evar_defined c -> Evar_defined (subst_mps s c)
-  in
-  { evi with
-      evar_concl = subst_mps s evi.evar_concl;
-      evar_hyps = subst_named_context_val s evi.evar_hyps;
-      evar_body = subst_evb evi.evar_body }
-
-let subst_evar_defs_light sub evd =
-  assert (Univ.is_initial_universes evd.universes.uctx_universes);
-  assert (List.is_empty evd.conv_pbs);
-  let map_info i = subst_evar_info sub i in
-  { evd with
-    undf_evars = EvMap.smartmap map_info evd.undf_evars;
-    defn_evars = EvMap.smartmap map_info evd.defn_evars;
-    metas = Metamap.smartmap (map_clb (subst_mps sub)) evd.metas; }
-
-let subst_evar_map = subst_evar_defs_light
-
 let cmap f evd = 
   { evd with
       metas = Metamap.map (map_clb f) evd.metas;
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 26e6bc50f2..54c5d9bf23 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -227,9 +227,6 @@ val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
-val subst_evar_defs_light : substitution -> evar_map -> evar_map
-(** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
-
 val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> 
   evar_map ->  evar_map -> evar_map
 (** spiwack: this function seems to somewhat break the abstraction. *)
@@ -600,5 +597,3 @@ val create_evar_defs      : evar_map -> evar_map
 (** Create an [evar_map] with empty meta map: *)
 
 val create_goal_evar_defs : evar_map -> evar_map
-
-val subst_evar_map : substitution -> evar_map -> evar_map