diff options
| author | notin | 2007-03-21 14:02:37 +0000 |
|---|---|---|
| committer | notin | 2007-03-21 14:02:37 +0000 |
| commit | 3c3c70e20208262952b90ab4abb5090a62f16b64 (patch) | |
| tree | bfa14d328a9a48623d93f025edeb9ba04ea33361 | |
| parent | f35b7d420a31d98c82a4ee3bef631c9fa1b846f9 (diff) | |
Suppression des sauts de lignes superflus de Show Script (test-suite/output/Tactics.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9725 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 = |