diff options
| -rw-r--r-- | parsing/tactic_printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index f8ba788a16..b0e487ac5f 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -189,7 +189,7 @@ let print_treescript nochange sigma pf = | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - hv indent (pr_rule_dot r ++ fnl() ++ prlist_with_sep fnl aux spfl) + hv indent (pr_rule_dot r ++ prlist_with_sep fnl aux spfl) in hov 0 (aux pf) let rec print_info_script sigma osign pf = |