From a70a76ff39ef6a003d2cd517900d5b62b3914767 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 7 Apr 2004 22:50:46 +0000
Subject: Loic code to pretty-print the generated proof-tree debranched (since
 it generates not well-formed XML files). An hook is left in xmlcommand.ml to
 register a pretty-printer function once a fixed implementation is provided.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/proofTree2Xml.ml4 | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 84091f0abd..20c0798a79 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -192,4 +192,6 @@ Pp.ppnl (Pp.(++) (Pp.str
 
 
 (* Hook registration *)
+(* CSC: debranched since it is bugged
 Xmlcommand.set_print_proof_tree print_proof_tree;;
+*)
-- 
cgit v1.2.3