aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_vo2xml.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coq_vo2xml.ml')
-rw-r--r--tools/coq_vo2xml.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coq_vo2xml.ml b/tools/coq_vo2xml.ml
index 9b47fed03..5f71fca39 100644
--- a/tools/coq_vo2xml.ml
+++ b/tools/coq_vo2xml.ml
@@ -65,7 +65,6 @@ let compile command args file =
Unix.stdin
in
let oc = open_out tmpfile in
- Printf.fprintf oc "Require Xml.\n" ;
Printf.fprintf oc "Require %s.\n" modulename;
Printf.fprintf oc "Print XML Module Disk \"%s\" %s.\n" !xml_library_root
modulename;