Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4e

Attempt to adapt .el files too.
doc/refman/RefMan-uti.tex has still to be fixed.

6 files changed, 17 insertions, 17 deletions

diff --git a/Makefile.build b/Makefile.build
index 3ebf79845..563c35595 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -667,7 +667,7 @@ install-coq-manpages:
 
 install-emacs:
 	$(MKDIR) $(FULLEMACSLIB)
-	$(INSTALLLIB) tools/coq-db.el tools/coq-font-lock.el tools/coq-syntax.el tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
+	$(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/coq-inferior.el $(FULLEMACSLIB)
 
 # command to update TeX' kpathsea database
 #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
diff --git a/configure b/configure
index 1069ad414..417934206 100755
--- a/configure
+++ b/configure
@@ -1117,7 +1117,7 @@ $BUILDLDPATH
 #        do_Makefile will reside
 # LIBDIR=path where the Coq library will reside
 # MANDIR=path where to install manual pages
-# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
+# EMACSDIR=path where to put Coq's Emacs mode (gallina.el)
 BINDIR="$BINDIR"
 COQLIBINSTALL="$LIBDIR"
 CONFIGDIR="$CONFIGDIR"
diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el
index d4f96a16e..15849859b 100644
--- a/tools/coq-inferior.el
+++ b/tools/coq-inferior.el
@@ -46,7 +46,7 @@
 
 ;;; Installation:
 
-;; You need to have coq.el already installed (it comes with the
+;; You need to have gallina.el already installed (it comes with the
 ;; standard Coq distribution) in order to use this code.  Put this
 ;; file somewhere in you load-path and add the following lines in your
 ;; "~/.emacs":
diff --git a/tools/gallina-db.el b/tools/gallina-db.el
index 5081b10b6..dd2bdf3ff 100644
--- a/tools/gallina-db.el
+++ b/tools/gallina-db.el
@@ -1,4 +1,4 @@
-;;; coq-db.el --- coq keywords database utility functions
+;;; gallina-db.el --- coq keywords database utility functions
 ;;
 ;; Author: Pierre Courtieu <courtieu@lri.fr>
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
@@ -231,9 +231,9 @@ Required so that 'proof-solve-tactics-face is a proper facename")
 
 
 
-(provide 'coq-db)
+(provide 'gallina-db)
 
-;;; coq-db.el ends here
+;;; gallina-db.el ends here
 
 ;** Local Variables: ***
 ;** fill-column: 80 ***
diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el
index 8630fb3a9..cbf4433be 100644
--- a/tools/gallina-syntax.el
+++ b/tools/gallina-syntax.el
@@ -1,14 +1,14 @@
-;; coq-syntax.el Font lock expressions for Coq
+;; gallina-syntax.el Font lock expressions for Coq
 ;; Copyright (C) 1997-2007 LFCS Edinburgh. 
 ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
 
-;; coq-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp
+;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp
 
 ;(require 'proof-syntax)
 ;(require 'proof-utils)                  ; proof-locate-executable
-(require 'coq-db)
+(require 'gallina-db)
 
 
 
@@ -618,7 +618,7 @@
 ;; proof-done-advancing-save in generic/proof-script.el) for coq <
 ;; 8.0. It is the test when looking backward the start of the proof.
 ;; It is NOT used for coq > v8.1
-;; (coq-find-and-forget in coq.el uses state numbers, proof numbers and
+;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and
 ;; lemma names given in the prompt)
 
 ;; compatibility with v8.0, will delete it some day
@@ -950,7 +950,7 @@ Used by `coq-goal-command-p'"
   (modify-syntax-entry ?\' "_")
   (modify-syntax-entry ?\| ".")
 
-;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug
+;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug
   (modify-syntax-entry ?\. ".") 
 
   (condition-case nil
@@ -969,8 +969,8 @@ Used by `coq-goal-command-p'"
  		  1))
  	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
 
-(provide 'coq-syntax)
- ;;; coq-syntax.el ends here
+(provide 'gallina-syntax)
+ ;;; gallina-syntax.el ends here
 
 ; Local Variables: ***
 ; indent-tabs-mode: nil ***
diff --git a/tools/gallina.el b/tools/gallina.el
index f4c4b033d..a70553673 100644
--- a/tools/gallina.el
+++ b/tools/gallina.el
@@ -1,9 +1,9 @@
-;; coq.el --- Coq mode editing commands for Emacs
+;; gallina.el --- Coq mode editing commands for Emacs
 ;;
 ;; Jean-Christophe Filliatre, march 1995
 ;; Honteusement pompé de caml.el, Xavier Leroy, july 1993.
 ;;
-;; modified by Marco Maggesi <maggesi@math.unifi.it> for coq-inferior
+;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior
 
 ; compatibility code for proofgeneral files
 (require 'coq-font-lock)
@@ -137,6 +137,6 @@ Does nothing otherwise."
              (coq-in-indentation))
         (backward-delete-char-untabify coq-mode-indentation))))
 
-;;; coq.el ends here
+;;; gallina.el ends here
 
-(provide 'coq)
+(provide 'gallina)