diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-14 16:38:19 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-14 16:38:19 +0000 |
| commit | 6c0af6104d41762220a1d613d2331e7a0294df80 (patch) | |
| tree | 5228691b8086d86f1c731d8dac608c27e48f89a6 /plugins/xml | |
| parent | d642755f1e6f036b521af63acc17338668d8fe0d (diff) | |
Bug 2636 - Move string_of_ppcmds to Pp
by Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
| -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 |