diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | distrib/Makefile | 13 | ||||
| -rw-r--r-- | distrib/debian/coq.emacsen-startup | 5 | ||||
| -rwxr-xr-x | distrib/debian/rules | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | man/coq-tex.1 (renamed from tools/coq-tex.1) | 0 | ||||
| -rw-r--r-- | man/coqc.1 | 48 | ||||
| -rw-r--r--[-rwxr-xr-x] | man/coqdep.1 (renamed from tools/coqdep.1) | 0 | ||||
| -rw-r--r-- | man/coqtop.1 | 38 | ||||
| -rw-r--r-- | man/coqtop.byte.1 | 35 | ||||
| -rw-r--r-- | man/coqtop.opt.1 | 35 | ||||
| -rw-r--r--[-rwxr-xr-x] | man/gallina.1 (renamed from tools/gallina.1) | 0 |
11 files changed, 170 insertions, 9 deletions
@@ -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 255e1572d..9fa9044e9 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 d1369ae6c..d5cd0ae1f 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 06927dc3f..2dbe6b1dd 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/tools/coq-tex.1 b/man/coq-tex.1 index 737de70a9..737de70a9 100755..100644 --- a/tools/coq-tex.1 +++ b/man/coq-tex.1 diff --git a/man/coqc.1 b/man/coqc.1 new file mode 100644 index 000000000..96fbcc2ae --- /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/tools/coqdep.1 b/man/coqdep.1 index 01d080fc2..01d080fc2 100755..100644 --- a/tools/coqdep.1 +++ b/man/coqdep.1 diff --git a/man/coqtop.1 b/man/coqtop.1 new file mode 100644 index 000000000..5662a3dc4 --- /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 000000000..4248c9e3d --- /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 000000000..8b6b362a1 --- /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/tools/gallina.1 b/man/gallina.1 index 8c607216e..8c607216e 100755..100644 --- a/tools/gallina.1 +++ b/man/gallina.1 |