Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4e

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

4 files changed, 15 insertions, 15 deletions

diff --git a/tools/coq-inferior.el b/tools/coq-inferior.el
index d4f96a16eb..15849859b6 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 5081b10b6c..dd2bdf3ff5 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 8630fb3a9c..cbf4433be5 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 f4c4b033d3..a705536738 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)