summaryrefslogtreecommitdiff
path: root/man/coq-parser.1
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
commit113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch)
treec260a140410c796f113584a2f7e6b9b7f6e00aa5 /man/coq-parser.1
parent870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff)
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
Diffstat (limited to 'man/coq-parser.1')
-rw-r--r--man/coq-parser.130
1 files changed, 30 insertions, 0 deletions
diff --git a/man/coq-parser.1 b/man/coq-parser.1
new file mode 100644
index 00000000..23dc8201
--- /dev/null
+++ b/man/coq-parser.1
@@ -0,0 +1,30 @@
+.TH COQ 1 "April 25, 2001"
+
+.SH NAME
+coq\-parser \- Coq parser
+
+
+.SH SYNOPSIS
+.B coq\-parser
+[
+.B options
+]
+
+.SH DESCRIPTION
+
+.B parser
+is a program reading Coq proof developments and outputing them in the
+structured format given in the INRIA technical report RT154. This
+program is not for the casual user.
+
+.SH SEE ALSO
+
+.BR coq\-interface (1),
+.BR coqc (1),
+.BR coqtop (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr