- Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.byte

- Deplacement pages de tools/ vers man/
- Modif distrib/Makefile pour Debian
- Modif mode emacs pour Debian


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1710 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 0 insertions, 381 deletions

diff --git a/tools/coq-tex.1 b/tools/coq-tex.1
deleted file mode 100755
index 737de70a9d..0000000000
--- a/tools/coq-tex.1
+++ /dev/null
@@ -1,125 +0,0 @@
-.TH COQ-TEX 1 "29 March 1995"
-
-.SH NAME
-coq-tex \- Process Coq phrases embedded in LaTeX files
-
-.SH SYNOPSIS
-.B coq-tex
-[
-.BI \-o \ output-file
-]
-[
-.BI \-n \ line-width
-]
-[
-.BI \-image \ coq-image
-]
-[
-.B -w
-]
-[
-.B -v
-]
-[
-.B -sl
-]
-[
-.B -hrule
-]
-[
-.B -small
-]
-.I input-file ...
-
-
-.SH DESCRIPTION
-
-The
-.B coq-tex
-filter extracts Coq phrases embedded in LaTeX files, evaluates
-them, and insert the outcome of the evaluation after each phrase.
-
-Three LaTeX environments are provided to include Coq code in
-the input files:
-.TP
-.B coq_example
-The phrases between \\begin{coq_example} and \\end{coq_example} are
-evaluated and copied into the output file. Each phrase is followed by
-the response of the toplevel loop.
-.TP
-.B coq_example*
-The phrases between \\begin{coq_example*} and \\end{coq_example*} are
-evaluated and copied into the output file. The responses of the
-toplevel loop are discarded.
-.TP
-.B coq_eval
-The phrases between \\begin{coq_eval} and \\end{coq_eval} are
-silently evaluated. They are not copied into the output file, and the
-responses of the toplevel loop are discarded.
-.PP
-The resulting LaTeX code is stored in the file
-.IR file \&.v.tex
-if the input file has a name of the form
-.IR file \&.tex,
-otherwise the name of the output file is the name of the input file
-with `.v.tex' appended.
-
-The files produced by
-.B coq-tex
-can be directly processed by LaTeX. 
-Both the Coq phrases and the toplevel output are typeset in
-typewriter font.
-
-.SH OPTIONS
-
-.TP
-.BI \-o \ output-file
-Specify the name of a file where the LaTeX output is to be stored. A
-dash `-' causes the LaTeX output to be printed on standard output.
-.TP
-.BI \-n \ line-width
-Set the line width. The default is 72 characters. The responses of the
-toplevel loop are folded if they are longer than the line width. No
-folding is performed on the Coq input text.
-.TP
-.BI \-image \ coq-image
-Cause the file
-.IR coq-image
-to be executed to evaluate the Coq phrases. By default,
-this is the command 
-.IR coqtop
-without specifying any path which is used to evaluate the Coq phrases.
-.TP
-.B -w
-Cause lines to be folded on a space character whenever possible,
-avoiding word cuts in the output. By default, folding occurs at
-the line width, regardless of word cuts.
-.TP
-.B -v
-Verbose mode. Prints the Coq answers on the standard output.
-Useful to detect errors in Coq phrases.
-.TP
-.B -sl
-Slanted mode. The Coq answers are written in a slanted font.
-.TP
-.B -hrule
-Horizontal lines mode. The Coq parts are written between two
-horizontal lines.
-.TP
-.B -small
-Small font mode. The Coq parts are written in a smaller font.
-
-
-.SH CAVEATS
-The \\begin... and \\end... phrases must sit on a line by themselves,
-with no characters before the backslash or after the closing brace.
-Each Coq phrase must be terminated by `.' at the end of a line.
-Blank space is accepted between `.' and the newline, but any other
-character will cause coq-tex to ignore the end of the phrase,
-resulting in an incorrect shuffling of the responses into the phrases.
-(The responses ``lag behind''.)
-
-.SH SEE ALSO
-
-.B coqtop
-(1).
diff --git a/tools/coqdep.1 b/tools/coqdep.1
deleted file mode 100755
index 01d080fc2a..0000000000
--- a/tools/coqdep.1
+++ /dev/null
@@ -1,182 +0,0 @@
-.TH COQ 1 "28 March 1995" "Coq tools"
-
-.SH NAME
-coqdep \- Compute inter-module dependencies for Coq and Caml programs
-
-.SH SYNOPSIS
-.B coqdep
-[
-.BI \-w
-]
-[
-.BI \-I \ directory
-]
-[
-.BI \-coqlib \ directory
-]
-[
-.BI \-c
-]
-[
-.BI \-i
-]
-[
-.BI \-D
-]
-.I filename ...
-.I directory ...
-
-.SH DESCRIPTION
-
-.B coqdep
-compute inter-module dependencies for Coq and Caml programs,
-and prints the dependencies on the standard output in a format
-readable by make.
-When a directory is given as argument, it is recursively looked at.
-
-Dependencies of Coq modules are computed by looking at
-.IR Require \&
-commands (Require, Require Export, Require Import, Require Implementation),
-and
-.IR Declare \& 
-.IR ML \& 
-.IR Module \&
-commands. Dependencies relative to modules from the Coq library are not
-printed.
-
-Dependencies of Caml modules are computed by looking at
-.IR open \&
-directives and the dot notation
-.IR module.value \&.
-
-.SH OPTIONS
-
-.TP
-.BI \-c
-Prints the dependencies of Caml modules.
-(On Caml modules, the behaviour is exactly the same as cldepend,
-except that nested comments and strings are correctly handled).
-.TP
-.BI \-w
-Prints a warning if a Coq command
-.IR Declare \& 
-.IR ML \& 
-.IR Module \&
-is incorrect. (For instance, you wrote `Declare ML Module "A".',
-but the module A contains #open "B"). The correct command is printed
-(see option -D). The warning is printed on standard error.
-.TP
-.BI \-i
-Prints also the dependencies for .vi files (Coq specification modules).
-.TP
-.BI \-D
-This commands looks for every command
-.IR Declare \& 
-.IR ML \& 
-.IR Module \&
-of each Coq file given as argument and complete (if needed)
-the list of Caml modules. The new command is printed on
-the standard output. No dependency is computed with this option.
-.TP 
-.BI \-I \ directory
-The files .v .ml .mli of the directory
-.IR directory \&
-are taken into account during the calculus of dependencies,
-but their own dependencies are not printed.
-.TP 
-.BI \-coqlib \ directory
-Indicates where is the Coq library. The default value has been
-determined at installation time, and therefore this option should not
-be used.
-
-
-.SH SEE ALSO
-
-.BR ocamlc (1),
-.BR coqc (1),
-.BR make (1).
-.br
-
-.SH NOTES
-
-Lexers (for Coq and Caml) correctly handle nested comments
-and strings.
-
-The treatment of symbolic links is primitive.
-
-If two files have the same name, in two different directories,
-a warning is printed on standard error.
-
-There is no way to limit the scope of the recursive search for
-directories.
-
-.SH EXAMPLES
-
-.LP
-Consider the files (in the same directory):
-
-	A.ml B.ml C.ml D.ml X.v Y.v and Z.v
-
-where
-.TP
-.BI \+ 
-D.ml contains the commands `#open "A"', `#open "B"' and `type t = C__t' ;
-.TP
-.BI \+
-Y.v contains the command `Require X' ;
-.TP
-.BI \+
-Z.v contains the commands `Require X' and `Declare ML Module "D"'.
-.LP
-To get the dependencies of the Coq files:
-.IP
-.B
-example% coqdep -I . *.v
-.RS
-.sp .5
-.nf
-.B Z.vo: Z.v ./X.vo ./D.zo
-.B Y.vo: Y.v ./X.vo
-.B X.vo: X.v
-.fi
-.RE
-.br
-.ne 7
-.LP
-With a warning:
-.IP
-.B
-example% coqdep -w -I . *.v
-.RS
-.sp .5
-.nf
-.B Z.vo: Z.v ./X.vo ./D.zo
-.B Y.vo: Y.v ./X.vo
-.B X.vo: X.v
-### Warning : In file Z.v, the ML modules declaration should be
-### Declare ML Module "A" "B" "C" "D".
-.fi
-.RE
-.br
-.ne 7
-.LP
-To get only the Caml dependencies:
-.IP
-.B
-example% coqdep -c -I . *.ml
-.RS
-.sp .5
-.nf
-.B D.zo: D.ml ./A.zo ./B.zo ./C.zo
-.B C.zo: C.ml
-.B B.zo: B.ml
-.B A.zo: A.ml
-.fi
-.RE
-.br
-.ne 7
-
-.SH BUGS
-
-Please report any bug to
-.B coq-bugs@pauillac.inria.fr
diff --git a/tools/gallina.1 b/tools/gallina.1
deleted file mode 100755
index 8c607216ed..0000000000
--- a/tools/gallina.1
+++ /dev/null
@@ -1,74 +0,0 @@
-.TH COQ 1 "29 March 1995" "Coq tools"
-
-.SH NAME
-gallina \- extracts specification from Coq vernacular files
-
-.SH SYNOPSIS
-.B gallina
-[
-.BI \-
-]
-[
-.BI \-stdout
-]
-[
-.BI \-nocomments
-]
-.I file ...
-
-.SH DESCRIPTION
-
-.B gallina 
-takes Coq files as arguments and builds the corresponding
-specification files.
-The Coq file
-.IR foo.v \&
-gives bearth to the specification file
-.IR foo.g. \&
-The suffix '.g' stands for Gallina.
-
-For that purpose, gallina removes all commands that follow a
-"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it
-reaches a command "Abort.", "Save.", "Qed.", "Defined." or "Proof
-<...>.". It also removes every "Hint", "Syntax",
-"Immediate"  or "Transparent" command.
-
-Files without the .v suffix are ignored.
-
-
-.SH OPTIONS
-
-.TP
-.BI \-stdout
-Prints the result on standard output.
-.TP
-.BI \-
-Coq source is taken on standard input. The result is printed on
-standard output.
-.TP
-.BI \-nocomments
-Comments are removed in the *.g file.
-
-.SH NOTES
-
-Nested comments are correctly handled. In particular, every command
-"Save." or "Abort." in a comment is not taken into account.
-
-
-.SH BUGS
-
-Please report any bug to
-.B coq@pauillac.inria.fr
-
-
-
-
-
-
-	
-
-	
-
-	
-
-