Merge remote-tracking branch 'github/pr/172' into trunk

Was PR#172: alternate path separators in typeclass debug output.

1 files changed, 10 insertions, 1 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 0abfd342d..a85afcbf0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -498,7 +498,16 @@ let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
-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)
 
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in