diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 19:18:46 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-11 19:18:46 +0000 |
| commit | 1d651163f5a0d5cc9c06059e29332c493ec70664 (patch) | |
| tree | f134986dfb75947cd1a83a9721a5fc20f4077305 /kernel/mod_subst.ml | |
| parent | b6451f561214b5bb7a4206b0a096b0cbbb76a25b (diff) | |
Mod_subst: an unused function
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14551 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_subst.ml')
| -rw-r--r-- | kernel/mod_subst.ml | 4 |
1 files changed, 0 insertions, 4 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 -> |