From 1d651163f5a0d5cc9c06059e29332c493ec70664 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 11 Oct 2011 19:18:46 +0000 Subject: Mod_subst: an unused function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14551 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_subst.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel/mod_subst.ml') 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 -> -- cgit v1.2.3