From 4a8188a2b460ab014379c508abac933690b48555 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 6 Oct 2012 10:08:27 +0000
Subject: Clean-up : no more Proof_type.proof_tree

 Btw, remove unused code in the xml plugin and in Tactic_printer

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/xmlcommand.mli | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'plugins/xml/xmlcommand.mli')

diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
index ec50d62348..8e6254efc0 100644
--- a/plugins/xml/xmlcommand.mli
+++ b/plugins/xml/xmlcommand.mli
@@ -26,14 +26,3 @@ val print_ref : Libnames.reference -> string option -> unit
 (*  where dest is either None (for stdout) or (Some filename) *)
 (* pretty prints via Xml.pp the proof in progress on dest     *)
 val show : string option -> unit
-
-(* set_print_proof_tree f                                      *)
-(*  sets a callback function f to export the proof_tree to XML *)
-val set_print_proof_tree :
-    (string ->
-     Evd.evar_map ->
-     Proof_type.proof_tree ->
-     Term.constr Proof2aproof.ProofTreeHash.t ->
-     Proof_type.proof_tree Proof2aproof.ProofTreeHash.t ->
-     string Acic.CicHash.t -> Xml.token Stream.t) ->
-    unit
-- 
cgit v1.2.3