aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-22 15:31:12 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-23 12:09:14 +0200
commit74ddca99c649f2f8c203582a9b82bddf64fb6b52 (patch)
treef23aa6340c2630619864666ef5eed257d3d765d9 /kernel/mod_subst.ml
parentd23c7539887366202bc370d0f80c26a557486e1c (diff)
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
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)