From 30b58d43e48569afb50a35d3915ec7d453a61f5d Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Tue, 17 Dec 2013 18:26:48 +0100 Subject: Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4e Attempt to adapt .el files too. doc/refman/RefMan-uti.tex has still to be fixed. --- Makefile.build | 2 +- configure | 2 +- tools/coq-inferior.el | 2 +- tools/gallina-db.el | 6 +++--- tools/gallina-syntax.el | 14 +++++++------- tools/gallina.el | 8 ++++---- 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 ;; 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 -;; 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 for coq-inferior +;; modified by Marco Maggesi 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) -- cgit v1.2.3