summaryrefslogtreecommitdiff
path: root/debian/coq_makefile.1
diff options
context:
space:
mode:
Diffstat (limited to 'debian/coq_makefile.1')
-rw-r--r--debian/coq_makefile.196
1 files changed, 0 insertions, 96 deletions
diff --git a/debian/coq_makefile.1 b/debian/coq_makefile.1
deleted file mode 100644
index 7890fde1..00000000
--- a/debian/coq_makefile.1
+++ /dev/null
@@ -1,96 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coq_makefile \- The Coq Proof Assistant makefile generator
-
-
-.SH SYNOPSIS
-.B coq_makefile
-[
-.B options
-]
-[
-.I subdirectory
-]
-[
-.I file.v
-]
-[
-.I file.ml
-]
-
-.SH DESCRIPTION
-
-.B coq_makefile
-is a makefile generator for Coq proof developments.
-
-.SH OPTIONS
-
-.TP
-.I subdirectory
-Subdirectory that should be "made".
-.TP
-.I file.v
-Coq file to be compiled.
-.TP
-.I file.ml
-ML file to be compiled.
-.TP
-.B \-h,\ \-\-help
-Will give you a description of the whole list of options of
-.BR coq_makefile .
-.TP
-.BI \-custom\ command\ dependencies\ file
-Add target
-.I file
-with command
-.I command
-and dependencies
-.I dependencies.
-.TP
-.BI \-I dir
-Look for dependencies in
-.IR dir .
-.TP
-.BI \-R\ physicalpath\ logicalpath
-Look for dependencies recursively starting from.
-.IR physicalpath .
-The logical path associated to the physical path is
-.IR logicalpath .
-.TP
-.IB VARIABLE\ =\ value
-Add the variable definition "VARIABLE=value".
-.TP
-.B \-byte
-Compile with byte-code version of
-.BR coq (1).
-.TP
-.B \-opt
-Compile with native-code version of
-.BR coq (1).
-.TP
-.B \-impredicative\-set
-Compile with option
-.B \-impredicative\-set
-of
-.BR coq (1).
-.TP
-.B
-.BI \-f\ file
-Take the contents of file as arguments.
-.TP
-.BI \-o\ file
-Output should go in file
-.IR file .
-
-
-.SH SEE ALSO
-
-.BR coqtop (1),
-.BR coqtc (1),
-.BR coqdep (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr