diff options
| author | notin | 2006-09-28 17:44:35 +0000 |
|---|---|---|
| committer | notin | 2006-09-28 17:44:35 +0000 |
| commit | 5865dad7bae73b13096a62e3657b02e13771524a (patch) | |
| tree | 1b6f0885daa06559697914bb279a824d9e74f9b9 | |
| parent | ee38b617146ad8b6b2e318e3037688f6008556f2 (diff) | |
Suppression des lignes vides dans l'affichage des scripts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9186 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 e1cc8463c3..484b30e985 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -188,7 +188,7 @@ let print_treescript nochange sigma pf = (print_script nochange sigma) spfl ) | Some(r,spfl) -> (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ fnl () ++ + pr_rule_dot r ++ begin if List.length spfl > 1 then fnl () ++ |