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 ----
 kernel/mod_subst.mli | 4 ----
 2 files changed, 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 275c6e6775..f32198f800 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 e06cc816da..90b3d8c692 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
 
-- 
cgit v1.2.3