From b002b817ce305be3ba753dc1634a01b008b243bd Mon Sep 17 00:00:00 2001 From: courant Date: Wed, 25 Apr 2001 07:35:06 +0000 Subject: - 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 --- Makefile | 3 +- distrib/Makefile | 13 ++- distrib/debian/coq.emacsen-startup | 5 + distrib/debian/rules | 2 +- man/coq-tex.1 | 125 +++++++++++++++++++++++++ man/coqc.1 | 48 ++++++++++ man/coqdep.1 | 182 +++++++++++++++++++++++++++++++++++++ man/coqtop.1 | 38 ++++++++ man/coqtop.byte.1 | 35 +++++++ man/coqtop.opt.1 | 35 +++++++ man/gallina.1 | 74 +++++++++++++++ tools/coq-tex.1 | 125 ------------------------- tools/coqdep.1 | 182 ------------------------------------- tools/gallina.1 | 74 --------------- 14 files changed, 551 insertions(+), 390 deletions(-) create mode 100644 man/coq-tex.1 create mode 100644 man/coqc.1 create mode 100644 man/coqdep.1 create mode 100644 man/coqtop.1 create mode 100644 man/coqtop.byte.1 create mode 100644 man/coqtop.opt.1 create mode 100644 man/gallina.1 delete mode 100755 tools/coq-tex.1 delete mode 100755 tools/coqdep.1 delete mode 100755 tools/gallina.1 diff --git a/Makefile b/Makefile index 18ebe16a6b..946a54453b 100644 --- a/Makefile +++ b/Makefile @@ -596,7 +596,8 @@ install-library: $(MKDIR) $(FULLEMACSLIB) cp tools/coq.el $(FULLEMACSLIB) -MANPAGES=tools/coq-tex.1 tools/coqdep.1 tools/gallina.1 +MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ + man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 install-manpages: $(MKDIR) $(FULLMANDIR)/man1 diff --git a/distrib/Makefile b/distrib/Makefile index 255e1572d0..9fa9044e9a 100644 --- a/distrib/Makefile +++ b/distrib/Makefile @@ -262,10 +262,9 @@ patch-ftp-install: prep-ftp-install cp patch-${VERSION}-$(PREVIOUSVERSION).gz ${FTPDIR}/V${VERSION}/ chmod g+w ${FTPDIR}/V${VERSION}/patch-${VERSION}-$(PREVIOUSVERSION).gz -deb: - rm -rf ../debian ../../coq-7.0.0.orig ../../coq_7.0.0_* ../../coq_7.0.0.* - cd ../.. ; cp -a coq-7.0.0 coq-7.0.0.orig - cp -a debian .. - cd .. ; dpkg-buildpackage -rfakeroot -uc -us -# rm -rf ../debian - +deb: ${COQPACKAGE}.tar.gz + tar xzf ${COQPACKAGE}.tar.gz + mv ${COQPACKAGE} ${COQPACKAGE}.orig + tar xzf ${COQPACKAGE}.tar.gz + cd ${COQPACKAGE} ; cp -a distrib/debian . + cd ${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us diff --git a/distrib/debian/coq.emacsen-startup b/distrib/debian/coq.emacsen-startup index d1369ae6cb..d5cd0ae1f7 100644 --- a/distrib/debian/coq.emacsen-startup +++ b/distrib/debian/coq.emacsen-startup @@ -11,8 +11,13 @@ ;; xemacs19, emacs20, xemacs20...). The compiled code is then ;; installed in a subdirectory of the respective site-lisp directory. ;; We have to add this to the load-path: + (setq load-path (cons (concat "/usr/share/" (symbol-name flavor) "/site-lisp/coq") load-path)) +(autoload 'coq-mode "coq" "Coq major mode" t) +(setq-default auto-mode-alist + (cons '("\\.v" . coq-mode) + auto-mode-alist)) diff --git a/distrib/debian/rules b/distrib/debian/rules index 06927dc3fa..2dbe6b1dda 100755 --- a/distrib/debian/rules +++ b/distrib/debian/rules @@ -12,7 +12,7 @@ configure: configure-stamp configure-stamp: dh_testdir # Add here commands to configure the package. - ./configure --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp + ./configure --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq touch configure-stamp diff --git a/man/coq-tex.1 b/man/coq-tex.1 new file mode 100644 index 0000000000..737de70a9d --- /dev/null +++ b/man/coq-tex.1 @@ -0,0 +1,125 @@ +.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/man/coqc.1 b/man/coqc.1 new file mode 100644 index 0000000000..96fbcc2ae2 --- /dev/null +++ b/man/coqc.1 @@ -0,0 +1,48 @@ +.TH COQ 1 "April 24, 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 +Will give you a description of the whole list of options of coqc and +coqtop. + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coqdep.1 b/man/coqdep.1 new file mode 100644 index 0000000000..01d080fc2a --- /dev/null +++ b/man/coqdep.1 @@ -0,0 +1,182 @@ +.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/man/coqtop.1 b/man/coqtop.1 new file mode 100644 index 0000000000..5662a3dc48 --- /dev/null +++ b/man/coqtop.1 @@ -0,0 +1,38 @@ +.TH COQ 1 "April 24, 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 +Help. Will give you the complete list of options accepted by coqtop. + +.SH SEE ALSO + +.BR coqc (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1 new file mode 100644 index 0000000000..4248c9e3d5 --- /dev/null +++ b/man/coqtop.byte.1 @@ -0,0 +1,35 @@ +.TH COQ 1 "April 24, 2001" + +.SH NAME +coqtop.byte \- The bytecode Coq toplevel + + +.SH SYNOPSIS +.B coqtop.byte +[ +.B options +] +[ +.I file +] + +.SH DESCRIPTION + +.B coqopt.byte +is the bytecode version of Coq. It should not be called directly, but +only by +.B coqtop +and +.B coqc + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqc (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr + + diff --git a/man/coqtop.opt.1 b/man/coqtop.opt.1 new file mode 100644 index 0000000000..8b6b362a15 --- /dev/null +++ b/man/coqtop.opt.1 @@ -0,0 +1,35 @@ +.TH COQ 1 "April 24, 2001" + +.SH NAME +coqtop.opt \- The native-code Coq toplevel + + +.SH SYNOPSIS +.B coqopt.opt +[ +.B options +] +[ +.I file +] + +.SH DESCRIPTION + +.B coqopt.opt +is the native-code version of Coq. It should not be called directly, but +only by +.B coqtop +and +.B coqc + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqc (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr + + diff --git a/man/gallina.1 b/man/gallina.1 new file mode 100644 index 0000000000..8c607216ed --- /dev/null +++ b/man/gallina.1 @@ -0,0 +1,74 @@ +.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 + + + + + + + + + + + + + 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 - - - - - - - - - - - - - -- cgit v1.2.3