From 6c0af6104d41762220a1d613d2331e7a0294df80 Mon Sep 17 00:00:00 2001 From: pboutill Date: Mon, 14 Nov 2011 16:38:19 +0000 Subject: 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 --- plugins/xml/proofTree2Xml.ml4 | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'plugins/xml') 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 -- cgit v1.2.3