From f4cbb370c64b5ed187fa10abaed39319d5f0d28c Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 17 May 2016 12:16:15 -0400
Subject: alternate path separators in typeclass debug output (4736)

---
 tactics/class_tactics.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4855598989..311ae19719 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -275,7 +275,16 @@ let catchable = function
 
 let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
 
-let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
+(* 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)
 
 type autoinfo = { hints : hint_db; is_evar: existential_key option;
 		  only_classes: bool; unique : bool;
-- 
cgit v1.2.3