From a00a51f312720d1cfbc138664f6ea50b2d6fb3c6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Aug 2020 16:39:19 +0200
Subject: Remove dead code in dnets.

The boolean assumedly used to cut recursion was always set to true, since
its introduction in 64ac193.
---
 tactics/dn.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/tactics/dn.ml b/tactics/dn.ml
index 07eb49442a..ebe88cd221 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
@@ -83,13 +83,11 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
             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))
+                List.flatten(List.map (fun tm -> lookrec c tm) l))
                  (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.flatten (List.map (fun tm -> ZSet.elements (Trie.get tm)) (lookrec t tm))
 
   let pattern dna pat = path_of dna pat
 
-- 
cgit v1.2.3


From 41b407395ba6f2ce2db5dd9365c9cbcb04a4e7c0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Aug 2020 16:47:04 +0200
Subject: Clean up a bit the implemenation of dnets.

We use higher-level combinators instead of composition of low-level ones.
---
 tactics/dn.ml | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/tactics/dn.ml b/tactics/dn.ml
index ebe88cd221..571f2f450b 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -73,21 +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 -> lookrec c tm) 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 -> 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
 
-- 
cgit v1.2.3


From f50bbdc50b21083f65f0e415e7f2edff6f11e45f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Sep 2020 10:11:24 +0200
Subject: Remove unused API from Dn.

---
 tactics/btermdn.ml  | 2 --
 tactics/btermdn.mli | 1 -
 tactics/dn.ml       | 2 --
 tactics/dn.mli      | 2 --
 4 files changed, 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
-- 
cgit v1.2.3