aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d4251555d..7558a707e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -259,7 +259,7 @@ and erase_subtree depth = function
| (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
let pr_info_atom (d,pp) =
- str (String.make d ' ') ++ pp () ++ str "."
+ str (String.make (d-1) ' ') ++ pp () ++ str "."
let pr_info_trace = function
| (Info,_,{contents=(d,Some pp)::l}) ->