aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--INSTALL2
-rw-r--r--doc/refman/RefMan-uti.tex4
-rwxr-xr-xtools/README.emacs4
-rw-r--r--tools/coq-inferior.el4
-rw-r--r--tools/gallina.el4
5 files changed, 9 insertions, 9 deletions
diff --git a/INSTALL b/INSTALL
index 595fc606b..2b387b017 100644
--- a/INSTALL
+++ b/INSTALL
@@ -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.")