Remove obsolete manpages (now shipped upstream)

6 files changed, 2 insertions, 653 deletions

diff --git a/debian/coq-interface.1 b/debian/coq-interface.1
deleted file mode 100644
index 73e6eaa6..00000000
--- a/debian/coq-interface.1
+++ /dev/null
@@ -1,154 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coq-interface \-
-
-
-.SH SYNOPSIS
-.B coq-interface
-[
-.B options
-]
-
-.SH DESCRIPTION
-
-.B coq-interface
-is a Coq customized toplevel system for Coq containing some modules
-useful for the graphical interface. This program is not for the casual
-user.
-
-.SH OPTIONS
-
-.TP
-.B \-h
-Help. Will give you the complete list of options accepted by
-coq-interface (the same as coqtop).
-.BI \-I\  dir ,\ \-include\  dir
-Add directory dir in the include path.
-.TP
-.BI \-R\  dir\ coqdir
-Recursively map physical
-.I dir
-to logical
-.IR coqdir .
-.TP
-.B \-src
-Add source directories in the include path.
-.TP
-.BI \-is\  f ,\ \-inputstate\  f
-Read state from
-.IR f .coq.
-.TP
-.B \-nois
-Start with an empty state.
-.TP
-.BI \-outputstate\  f
-Write state in file
-.IR f .coq.
-.TP
-.BI \-load\-ml\-object\  f
-Load ML object file
-.IR f .
-.TP
-.BI \-load\-ml\-source\  f
-Load ML file
-.IR f .
-.TP
-.BI \-l\  f ,\ \-load\-vernac\-source\  f
-Load Coq file
-.IR f .v
-(Load
-.IR f .).
-.TP
-.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
-Load Coq file
-.IR f .v
-(Load Verbose
-.IR f .).
-.TP
-.BI \-load\-vernac\-object\  f
-Load Coq object file
-.IR f .vo.
-.TP
-.BI \-require\  f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
-.TP
-.BI \-compile\  f
-Compile Coq file
-.IR f .v
-(implies
-.BR \-batch ).
-.TP
-.BI \-compile\-verbose\  f
-Verbosely compile Coq file
-.IR f .v
-(implies
-.BR -batch ).
-.TP
-.B \-opt
-Run the native-code version of Coq or Coq_SearchIsos.
-.TP
-.B \-byte
-Run the bytecode version of Coq or Coq_SearchIsos.
-.TP
-.B \-where
-Print Coq's standard library location and exit.
-.TP
-.B -v
-Print Coq version and exit.
-.TP
-.B \-q
-Skip loading of rcfile.
-.TP
-.BI \-init\-file\  f
-Set the rcfile to
-.IR f .
-.TP
-.BI \-user\  u
-Use the rcfile of user
-.IR u .
-.TP
-.B \-batch
-Batch mode (exits just after arguments parsing).
-.TP
-.B \-boot
-Boot mode (implies
-.B \-q
-and
-.BR \-batch ).
-.TP
-.B \-emacs
-Tells Coq it is executed under Emacs.
-.TP
-.BI \-dump\-glob\  f
-Dump globalizations in file
-.I f
-(to be used by
-.BR coqdoc (1)).
-.TP
-.B \-impredicative\-set
-Set sort Set impredicative.
-.TP
-.B \-dont\-load\-proofs
-Don't load opaque proofs in memory.
-.TP
-.B \-xml
-Export XML files either to the hierarchy rooted in
-the directory
-.B COQ_XML_LIBRARY_ROOT
-(if set) or to stdout (if unset).
-
-.SH SEE ALSO
-
-.BR coqc (1),
-.BR coqdep (1),
-.BR coqtop (1),
-.BR parser (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
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
diff --git a/debian/coqc.1 b/debian/coqc.1
deleted file mode 100644
index baa04a88..00000000
--- a/debian/coqc.1
+++ /dev/null
@@ -1,172 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coqc \- The Coq Proof Assistant compiler
-
-
-.SH SYNOPSIS
-.B coqc
-[
-.B general \ Coq \ options
-]
-.I file
-
-
-.SH DESCRIPTION
-
-.B coqc
-is the batch compiler for the Coq Proof Assistant.
-The options are basically the same as coqtop(1).
-.IR file.v \&
-is the vernacular file to compile.
-.IR file \& 
-must be formed
-only with the characters `a` to  `Z`, `0`-`9` or `_` and must begin
-with a letter.
-The compiler produces an object file
-.IR file.vo \&.
-
-For interactive use of Coq, see 
-.BR coqtop(1).
-
-
-.SH OPTIONS
-
-.TP
-.BI \-h
-Show the whole list of options of coqc and coqtop.
-.TP
-.B \-verbose
-Compile verbosely.
-.TP
-.BI \-image\  f
-Specify an alternative executable for Coq.
-.TP
-.B \-t
-Keep temporary files.
-.TP
-.BI \-I\  dir ,\ \-include\  dir
-Add directory dir in the include path.
-.TP
-.BI \-R\  dir\ coqdir
-Recursively map physical dir to logical coqdir.
-.TP
-.B \-src
-Add source directories in the include path.
-.TP
-.BI \-is\  f ,\ \-inputstate\  f
-Read state from file
-.IR f .coq.
-.TP
-.B \-nois
-Start with an empty state.
-.TP
-.BI \-outputstate\  f
-Write state in file
-.IR f .coq.
-.TP
-.BR \-load\-ml\-object\  f
-Load ML object file
-.IR f .
-.TP
-.BI \-load\-ml\-source\  f
-Load ML file
-.IR f .
-.TP
-.BI \-l\  f ,\ \-load\-vernac\-source\  f
-Load Coq file
-.IR f .v
-(Load
-.IR f .).
-.TP
-.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
-Load Coq file
-.IR f .v
-(Load Verbose
-.IR f .).
-.TP
-.BI \-load\-vernac\-object\  f
-Load Coq object file
-.IR f .vo.
-.TP
-.BI \-require\  f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
-.TP
-.BI \-compile\  f
-Compile Coq file
-.IR f .v
-(implies
-.BR \-batch ).
-.TP
-.BI \-compile\-verbose\  f
-Verbosely compile Coq file
-.IR f .v
-(implies
-.BR \-batch ).
-.TP
-.B \-opt
-Run the native-code version of Coq or Coq_SearchIsos.
-.TP
-.B \-byte
-Run the bytecode version of Coq or Coq_SearchIsos.
-.TP
-.B \-where
-Print Coq's standard library location and exit.
-.TP
-.B \-v
-Print Coq version and exit.
-.TP
-.B \-q
-Skip loading of rcfile.
-.TP
-.BI \-init\-file\  f
-Set the rcfile to
-.IR f .
-.TP
-.BI \-user\  u
-Use the rcfile of user
-.IR u .
-.TP
-.B \-batch
-Batch mode (exits just after arguments parsing).
-.TP
-.B \-boot
-Boot mode (implies
-.B \-q
-and
-.BR \-batch ).
-.TP
-.B \-emacs
-Tells Coq it is executed under Emacs.
-.TP
-.BI \-dump\-glob\  f
-Dump globalizations in file
-.I f
-(to be used by
-.BR coqdoc (1)).
-.TP
-.B \-impredicative\-set
-Set sort Set impredicative.
-.TP
-.B \-dont\-load\-proofs
-Don't load opaque proofs in memory.
-.TP
-.B \-xml
-Export XML files either to the hierarchy rooted in
-the directory 
-.B COQ_XML_LIBRARY_ROOT
-(if set) or to stdout (if unset).
-
-.SH SEE ALSO
-
-.BR coqtop (1),
-.BR coq_makefile (1),
-.BR coqdep (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/debian/coqmktop.1 b/debian/coqmktop.1
deleted file mode 100644
index a35e436a..00000000
--- a/debian/coqmktop.1
+++ /dev/null
@@ -1,70 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coqmktop \- The Coq Proof Assistant user-tactics linker
-
-
-.SH SYNOPSIS
-.B coqmktop
-[
-.I options
-]
-.I files
-
-
-.SH DESCRIPTION
-
-.B coqmktop
-builds a new Coq toplevel extended with user-tactics.
-.IR files \&
-are the Objective Caml object or library files (i.e. with suffix .cmo,
-.cmx, .cma or .cmxa) to link with the Coq system.
-The linker produces an executable Coq toplevel which can be called
-directly or through coqc(1), using the -image option.
-
-.SH OPTIONS
-
-.TP
-.BI \-h
-Show a list of the available options.
-.TP
-.BI \-srcdir\  dir
-Specify where the Coq source files are.
-.TP
-.BI \-o\  exec\-fil
-Specify the name of the resulting toplevel.
-.TP
-.B \-opt
-Compile in native code.
-.TP
-.B \-full
-Link high level tactics.
-.TP
-.B \-top
-Build Coq on a ocaml toplevel (incompatible with
-.BR \-opt ).
-.TP
-.B \-searchisos
-Build a toplevel for SearchIsos.
-.TP
-.B \-ide
-Build a toplevel for the Coq IDE.
-.TP
-.BI \-R\  dir
-Specify recursively directories for Ocaml.
-.TP
-.B \-v8
-Link with V8 grammar.
-
-
-.SH SEE ALSO
-
-.BR coqtop (1),
-.BR ocamlmktop (1).
-.BR ocamlc (1).
-.BR ocamlopt (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/debian/coqtop.1 b/debian/coqtop.1
deleted file mode 100644
index b136a68b..00000000
--- a/debian/coqtop.1
+++ /dev/null
@@ -1,155 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coqtop \- The Coq Proof Assistant toplevel system
-
-
-.SH SYNOPSIS
-.B coqtop
-[
-.B options
-]
-
-.SH DESCRIPTION
-
-.B coqtop
-is the toplevel system of Coq, for interactive use.
-It reads phrases on the standard input, and prints results on the
-standard output.
-
-For batch-oriented use of Coq, see 
-.BR coqc (1).
-
-
-.SH OPTIONS
-
-.TP
-.B \-h
-Show the complete list of options accepted by coqtop.
-.TP
-.BI \-I\  dir ,\ \-include\  dir
-Add directory dir in the include path.
-.TP
-.BI \-R\  dir\ coqdir
-Recursively map physical dir to logical coqdir.
-.TP
-.B \-src
-Add source directories in the include path.
-.TP
-.BI \-is\  f ,\ \-inputstate\  f
-Read state from file
-.IR f .coq.
-.TP
-.B \-nois
-Start with an empty state.
-.TP
-.BI \-outputstate\  f
-Write state in file
-.IR f .coq.
-.TP
-.BR \-load\-ml\-object\  f
-Load ML object file
-.IR f .
-.TP
-.BI \-load\-ml\-source\  f
-Load ML file
-.IR f .
-.TP
-.BI \-l\  f ,\ \-load\-vernac\-source\  f
-Load Coq file
-.IR f .v
-(Load
-.IR f .).
-.TP
-.BI \-lv\  f ,\ \-load\-vernac\-source\-verbose\  f
-Load Coq file
-.IR f .v
-(Load Verbose
-.IR f .).
-.TP
-.BI \-load\-vernac\-object\  f
-Load Coq object file
-.IR f .vo.
-.TP
-.BI \-require\  f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
-.TP
-.BI \-compile\  f
-Compile Coq file
-.IR f .v
-(implies
-.BR \-batch ).
-.TP
-.BI \-compile\-verbose\  f
-Verbosely compile Coq file
-.IR f .v
-(implies
-.BR \-batch ).
-.TP
-.B \-opt
-Run the native-code version of Coq or Coq_SearchIsos.
-.TP
-.B \-byte
-Run the bytecode version of Coq or Coq_SearchIsos.
-.TP
-.B \-where
-Print Coq's standard library location and exit.
-.TP
-.B \-v
-Print Coq version and exit.
-.TP
-.B \-q
-Skip loading of rcfile.
-.TP
-.BI \-init\-file\  f
-Set the rcfile to
-.IR f .
-.TP
-.BI \-user\  u
-Use the rcfile of user
-.IR u .
-.TP
-.B \-batch
-Batch mode (exits just after arguments parsing).
-.TP
-.B \-boot
-Boot mode (implies
-.B \-q
-and
-.BR \-batch ).
-.TP
-.B \-emacs
-Tells Coq it is executed under Emacs.
-.TP
-.BI \-dump\-glob\  f
-Dump globalizations in file
-.I f
-(to be used by
-.BR coqdoc (1)).
-.TP
-.B \-impredicative\-set
-Set sort Set impredicative.
-.TP
-.B \-dont\-load\-proofs
-Don't load opaque proofs in memory.
-.TP
-.B \-xml
-Export XML files either to the hierarchy rooted in
-the directory 
-.B COQ_XML_LIBRARY_ROOT
-(if set) or to stdout (if unset).
-
-
-.SH SEE ALSO
-
-.BR coqc (1),
-.BR coq-tex (1),
-.BR coqdep (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/debian/rules b/debian/rules
index 7a986d94..640fceb8 100755
--- a/debian/rules
+++ b/debian/rules
@@ -101,16 +101,12 @@ install-stamp: build-stamp
 	cp debian/coqide.desktop debian/coqide/usr/share/applications
 
 	if [ -e opt-stamp ]; then \
-		cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \
+		cp man/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \
 		cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1; \
 	fi
+	cp man/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1
 	cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1
 	cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.byte.1
-	cp debian/coqc.1 debian/coq/usr/share/man/man1/coqc.1
-	cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1
-	cp debian/coq_makefile.1 debian/coq/usr/share/man/man1/coq_makefile.1
-	cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1
-	cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1
 
 	cp -r doc/stdlib/html debian/coq-libs/usr/share/doc/coq-libs/
 	cd debian/coq-libs/usr/share/doc/coq; ln -s ../coq-libs/html stdlib