diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-02 22:30:29 +0000 |
| commit | 401f17afa2e9cc3f2d734aef0d71a2c363838ebd (patch) | |
| tree | 7a3e0ce211585d4c09a182aad1358dfae0fb38ef /parsing/tactic_printer.ml | |
| parent | 15cb1aace0460e614e8af1269d874dfc296687b0 (diff) | |
Noise for nothing
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/tactic_printer.ml')
| -rw-r--r-- | parsing/tactic_printer.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 83dae3dce..b2b59f166 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -7,6 +7,7 @@ (************************************************************************) open Pp +open Errors open Util open Sign open Evd @@ -66,7 +67,7 @@ let rec print_proof sigma osign pf = spc () ++ str" BY " ++ hov 0 (pr_rule r) ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)) + hov 0 (prlist_with_sep fnl (print_proof sigma hyps) spfl)) let pr_change sigma gl = str"change " ++ @@ -110,11 +111,11 @@ let print_script ?(nochange=true) sigma pf = end | Some(Daimon,spfl) -> ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++ - prlist_with_sep pr_fnl print_prf spfl ) + prlist_with_sep fnl print_prf spfl ) | Some(rule,spfl) -> ((if nochange then (mt ()) else (pr_change sigma pf.goal ++ fnl ())) ++ pr_rule_dot_fnl rule ++ - prlist_with_sep pr_fnl print_prf spfl ) in + prlist_with_sep fnl print_prf spfl ) in print_prf pf (* printed by Show Script command *) @@ -140,7 +141,7 @@ let print_treescript ?(nochange=true) sigma pf = end | Some(Daimon,spfl) -> (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++ - prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl + prlist_with_sep fnl (print_script ~nochange sigma) spfl | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in (if nochange then mt () else pr_change sigma pf.goal ++ fnl ()) ++ @@ -162,7 +163,7 @@ let rec print_info_script sigma osign pf = print_info_script sigma (Environ.named_context_of_val sign) pf1) | _ -> (str"." ++ fnl () ++ - prlist_with_sep pr_fnl + prlist_with_sep fnl (print_info_script sigma (Environ.named_context_of_val sign)) spfl)) |