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