Remove dead code in Mod_subst.

2 files changed, 0 insertions, 20 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index b35b9dda31..8a4c359470 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -61,7 +61,6 @@ module Umap = struct
   let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2)
   let find_mp mp map = MPmap.find mp (fst map)
   let find_mbi mbi map = MBImap.find mbi (snd map)
-  let iter_mbi f map = MBImap.iter f (snd map)
   let fold fmp fmbi (m1,m2) i =
     MPmap.fold fmp m1 (MBImap.fold fmbi m2 i)
   let join map1 map2 = fold add_mp add_mbi map1 map2
@@ -551,20 +550,6 @@ let join subst1 subst2 =
   let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
   Umap.join subst2 subst
 
-let rec occur_in_path mbi = function
-  | MPbound bid' -> MBId.equal mbi bid'
-  | MPdot (mp1,_) -> occur_in_path mbi mp1
-  | _ -> false
-
-let occur_mbid mbi sub =
-  let check_one mbi' (mp,_) =
-    if MBId.equal mbi mbi' || occur_in_path mbi mp then raise Exit
-  in
-  try
-    Umap.iter_mbi check_one sub;
-    false
-  with Exit -> true
-
 type 'a substituted = {
   mutable subst_value : 'a;
   mutable subst_subst : substitution list;
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 2e5211c770..8416094063 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -165,11 +165,6 @@ val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
    names appearing in [c] *)
 val subst_mps : substitution -> constr -> constr
 
-(** [occur_*id id sub] returns true iff [id] occurs in [sub]
-   on either side *)
-
-val occur_mbid : MBId.t -> substitution -> bool
-
 (** [repr_substituted r] dumps the representation of a substituted:
     - [None, a] when r is a value
     - [Some s, a] when r is a delayed substitution [s] applied to [a] *)