diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-07 22:50:46 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-07 22:50:46 +0000 |
| commit | a70a76ff39ef6a003d2cd517900d5b62b3914767 (patch) | |
| tree | b17314f563fbcd311fa6d08bf7d3333c60d61c5d /contrib | |
| parent | 33c60bc1be8a4495d2f343d05938521f8194639a (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 84091f0ab..20c0798a7 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;; +*) |