Merge PR #13052: Clean up Dnet implementation

Reviewed-by: herbelin

4 files changed, 7 insertions, 18 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 07eb49442a..c587f91e54 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -62,10 +62,10 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
       pathrec []
 
   let tm_of tm lbl =
-    try [Trie.next tm lbl, true] with Not_found -> []
+    try [Trie.next tm lbl] with Not_found -> []
 
   let rec skip_arg n tm =
-    if Int.equal n 0 then [tm, true]
+    if Int.equal n 0 then [tm]
     else
       let labels = Trie.labels tm in
       let map lbl = match lbl with
@@ -73,23 +73,19 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
       | Some (_, m) ->
         skip_arg (pred n + m) (Trie.next tm lbl)
       in
-      List.flatten (List.map map labels)
+      List.map_append map labels
 
   let lookup tm dna t =
     let rec lookrec t tm =
       match dna t with
         | Nothing -> tm_of tm None
         | Label(lbl,v) ->
-            tm_of tm None@
-              (List.fold_left
-                 (fun l c ->
-                List.flatten(List.map (fun (tm, b) ->
-                                         if b then lookrec c tm
-                                         else [tm,b]) l))
-                 (tm_of tm (Some(lbl,List.length v))) v)
+          let fold accu c = List.map_append (fun tm -> lookrec c tm) accu in
+            tm_of tm None @
+              (List.fold_left fold (tm_of tm (Some (lbl, List.length v))) v)
         | Everything -> skip_arg 1 tm
     in
-    List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))
+    List.map_append (fun tm -> ZSet.elements (Trie.get tm)) (lookrec t tm)
 
   let pattern dna pat = path_of dna pat
 
@@ -99,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