diff options
-rw-r--r-- | kernel/mod_subst.ml | 4 | ||||
-rw-r--r-- | kernel/mod_subst.mli | 4 |
2 files changed, 0 insertions, 8 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 275c6e677..f32198f80 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -33,7 +33,6 @@ module Deltamap = struct let empty = MPmap.empty, KNmap.empty let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km) let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km) - let remove_mp mp (mm,km) = (MPmap.remove mp mm, km) let find_mp mp map = MPmap.find mp (fst map) let find_kn kn map = KNmap.find kn (snd map) let mem_mp mp map = MPmap.mem mp (fst map) @@ -113,9 +112,6 @@ let mind_in_delta mind resolver = kn_in_delta (user_mind mind) resolver let delta_of_mp resolve mp = try Deltamap.find_mp mp resolve with Not_found -> mp -let remove_mp_delta_resolver resolver mp = - Deltamap.remove_mp mp resolver - let rec find_prefix resolve mp = let rec sub_mp = function | MPdot(mp,l) as mp_sup -> diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index e06cc816d..90b3d8c69 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -55,10 +55,6 @@ val delta_of_mp : delta_resolver -> module_path -> module_path (** Extract the set of inlined constant in the resolver *) val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list -(** remove_mp is used for the computation of a resolver induced by Include P *) -val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver - - (** mem tests *) val mp_in_delta : module_path -> delta_resolver -> bool |