4 files changed, 0 insertions, 7 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index bacb5a7b8f..f721e9956b 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -186,7 +186,5 @@ struct
         (fun dn t ->
              Dn.lookup dn (bounded_constr_val_discr_st env sigma st) (t,!dnet_depth))
 
-  let app f dn = Dn.app f dn
-
 end
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index ab201a1872..01d68a8045 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -38,7 +38,6 @@ sig
   val rmv : t -> pattern -> Z.t -> t
 
   val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
-  val app : (Z.t -> unit) -> t -> unit
 end
 
 val dnet_depth : int ref
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
 
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 287aa2b257..85f9ef6dfb 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -38,6 +38,4 @@ sig
   val lookup : t -> 'term lookup_fun -> 'term
     -> Z.t list
 
-  val app : (Z.t -> unit) -> t -> unit
-
 end