aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
diff options
context:
space:
mode:
Diffstat (limited to 'man')
-rw-r--r--man/coq_vo2xml.169
1 files changed, 69 insertions, 0 deletions
diff --git a/man/coq_vo2xml.1 b/man/coq_vo2xml.1
new file mode 100644
index 000000000..21be67b77
--- /dev/null
+++ b/man/coq_vo2xml.1
@@ -0,0 +1,69 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq_vo2xml \- Exports the content of a Coq module to XML
+
+
+.SH SYNOPSIS
+.B coq_vo2xml
+[
+.B general \ Coq \ options
+]
+[
+.B -image
+.I f
+]
+[
+.B -t
+]
+[
+.B -xml-library-root
+.I d
+]
+.IR module " .\|.\|."
+
+
+.SH DESCRIPTION
+
+.B coq_vo2xml
+is a tool to export the content of a Coq module to XML.
+Because it executes coqtop(1), it recognizes a superset of its options.
+ones:
+.PP
+.B -image
+.IR f
+overrides the coqtop(1) executable with
+.IR f "."
+.PP
+.B -t
+does not remove the temporary file fed to coqtop(1).
+.PP
+.B -xml-library-root
+.IR d
+sets the path to the root of the XML library to
+.IR d ","
+overriding the value of $XML_ROOT_LIBRARY. The root of the XML library
+must be specified, either using the flag or setting the variable.
+.PP
+.IR module \&
+is the name of the module to export. The file module.vo will be searched in the
+Coq path by coqtop(1).
+The compiler produces a whole tree of XML files and directories rooted in the
+specified XML root library.
+
+.SH OPTIONS
+
+.TP
+.BI \-h
+Will give you a description of the whole list of options of coq_vo2xml,
+including the ones of coqtop(1).
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coq_makefile (1),
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr