diff options
| -rw-r--r-- | tactics/class_tactics.ml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0abfd342d2..a85afcbf09 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 |