aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_subst.ml')
-rw-r--r--kernel/mod_subst.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f0d1aca4d..9589c0656 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -38,7 +38,6 @@ module Deltamap = struct
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)
- let mem_kn kn map = KNmap.mem kn (snd map)
let fold_kn f map i = KNmap.fold f (snd map) i
let fold fmp fkn (mm,km) i =
MPmap.fold fmp mm (KNmap.fold fkn km i)