aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/eauto.ml43
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index aceba6e256..b62bf5820c 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -247,9 +247,6 @@ module SearchProblem = struct
with e when Logic.catchable_exception e ->
filter_tactics (glls,v) tacl
- let rec list_addn n x l =
- if n = 0 then l else x :: (list_addn (pred n) x l)
-
(* Ordering of states is lexicographic on depth (greatest first) then
number of remaining goals. *)
let compare s s' =