diff options
Diffstat (limited to 'plugins/xml/proofTree2Xml.ml4')
| -rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index c948ef58b..b0e4fcc69 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -14,11 +14,6 @@ let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; -let std_ppcmds_to_string s = - Pp.msg_with Format.str_formatter s; - Format.flush_str_formatter () -;; - let idref_of_id id = "v" ^ id;; (* Transform a constr to an Xml.token Stream.t *) @@ -156,7 +151,7 @@ Pp.ppnl (Pp.(++) (Pp.str | _ -> (****** la tactique employee *) let prtac = Pptactic.pr_tactic (Global.env()) in - let tac = std_ppcmds_to_string (prtac tactic_expr) in + let tac = Pp.string_of_ppcmds (prtac tactic_expr) in let tacname= first_word tac in let of_attribute = ("name",tacname)::("script",tac)::of_attribute in |