diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 14:34:16 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-20 14:34:16 +0200 |
commit | bb13eed99c310970ebb52c56ce785c1879caed66 (patch) | |
tree | 42b64004f5eae112cb5cc069ee39995d40dd11ad /tactics/class_tactics.ml | |
parent | 152bc6119aeed902a1f1f22e35e14596c616c93e (diff) | |
parent | bcfcf891563bcbf1d39a60275cabd695be162eee (diff) |
Merge PR #869: Enforce alternating separators in typeclass debug output
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r-- | tactics/class_tactics.ml | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9cf2f0bc0..6cb56d64f 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 |