aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorsacerdot2004-03-29 13:17:25 +0000
committersacerdot2004-03-29 13:17:25 +0000
commit4eaeba514ca5d2cfa42d57a1a8022c6337461356 (patch)
tree5e9c3d047c6f2771fefb2a6dcd25276ba9ee2a52
parent72620f6ac574cbbaefc40158c209ec0823df1c92 (diff)
Debug prints removed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5600 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/xml/xmlcommand.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index cddb0224d7..d8dfc4f3bc 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -868,11 +868,9 @@ let _ =
let _ =
Vernac.set_xml_start_library
(function () ->
- print_string "B";
theory_channel :=
Util.option_app (fun fn -> open_out (fn^".v"))
(theory_filename xml_library_root);
- print_string "C";
theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n";
theory_output_string "<html xmlns=\"http://www.w3.org/1999/xhtml\" xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">\n";
theory_output_string "<head>\n<style> A { text-decoration: none } </style>\n</head>\n")
@@ -909,7 +907,6 @@ let _ =
let _ =
Lib.set_xml_open_section
(fun id ->
- print_string "A";
let s = Names.string_of_id id in
theory_output_string ("<ht:SECTION name=\""^s^"\">"))
;;