From bcfcf891563bcbf1d39a60275cabd695be162eee Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 12 Jul 2017 11:16:09 -0400
Subject: format pairs of items for pr_depth to get alternating separators eval
 thunks once in prlist_sep_lastsep, make code clearer add typeclass debug
 output test

---
 tactics/class_tactics.ml | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7a85956538..d44e64b83c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -494,16 +494,15 @@ let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
-(* alternate separators in debug search path output *)
-let debug_seps = [| "." ; "-" |]
-let next_sep seps = 
-  let num_seps = Array.length seps in
-  let sep_index = ref 0 in
-  fun () ->
-    let sep = seps.(!sep_index) in
-    sep_index := (!sep_index + 1) mod num_seps;
-    str sep
-let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l)
+let pr_depth l = 
+  let rec fmt elts =
+    match elts with
+    | [] -> []
+    | [n] -> [string_of_int n]
+    | n1::n2::rest ->
+       (string_of_int n1 ^ "." ^ string_of_int n2) :: fmt rest
+  in
+  prlist_with_sep (fun () -> str "-") str (fmt (List.rev l))
 
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
-- 
cgit v1.2.3