diff options
-rw-r--r-- | INSTALL | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-uti.tex | 4 | ||||
-rwxr-xr-x | tools/README.emacs | 4 | ||||
-rw-r--r-- | tools/coq-inferior.el | 4 | ||||
-rw-r--r-- | tools/gallina.el | 4 |
5 files changed, 9 insertions, 9 deletions
@@ -161,7 +161,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). in you .emacs file: (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) + (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) 7- You can now clean all the sources. (You can even erase them.) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 85ed03430..07d711424 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -177,7 +177,7 @@ have been completely produced with {\tt coq-tex}. \subsection{The \Coq\ Emacs mode} -\Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides +\Coq\ comes with a Major mode for \emacs, {\tt gallina.el}. This mode provides syntax highlighting and also a rudimentary indentation facility in the style of the Caml \emacs\ mode. @@ -186,7 +186,7 @@ Add the following lines to your \verb!.emacs! file: \begin{verbatim} (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) + (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) \end{verbatim} The \Coq\ major mode is triggered by visiting a file with extension {\tt .v}, diff --git a/tools/README.emacs b/tools/README.emacs index 0d27b607f..4d8e3697a 100755 --- a/tools/README.emacs +++ b/tools/README.emacs @@ -10,14 +10,14 @@ Jean-Christophe Filliatre (jcfillia@lri.fr), CONTENTS: - coq.el A major mode for editing Coq files in Gnu Emacs + gallina.el A major mode for editing Coq files in Gnu Emacs USAGE: Add the following lines to your .emacs file: (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -(autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) +(autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) The Coq major mode is triggered by visiting a file with extension .v, or manually by M-x coq-mode. It gives you the correct syntax table for diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el index 15849859b..b79d97d66 100644 --- a/tools/coq-inferior.el +++ b/tools/coq-inferior.el @@ -52,7 +52,7 @@ ;; "~/.emacs": ;; ;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -;; (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) +;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) ;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) ;; (autoload 'run-coq-other-window "inferior-coq" ;; "Run an inferior Coq process in a new window." t) @@ -78,7 +78,7 @@ ;; From -0.0 to 1.0 brought into existence. -(require 'coq) +(require 'gallina) (require 'comint) (setq coq-program-name "coqtop") diff --git a/tools/gallina.el b/tools/gallina.el index a70553673..7af2d765f 100644 --- a/tools/gallina.el +++ b/tools/gallina.el @@ -8,8 +8,8 @@ ; compatibility code for proofgeneral files (require 'coq-font-lock) ; ProofGeneral files. remember to remove coq version tests in -; coq-syntax.el -(require 'coq-syntax) +; gallina-syntax.el +(require 'gallina-syntax) (defvar coq-mode-map nil "Keymap used in Coq mode.") |