aboutsummaryrefslogtreecommitdiff
path: root/tactics/dn.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/dn.ml')
-rw-r--r--tactics/dn.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 571f2f450b..c587f91e54 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -95,7 +95,5 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
let rmv tm p inf =
Trie.remove p (ZSet.singleton inf) tm
- let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm
-
end