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. --- tools/coq-inferior.el | 2 +- tools/gallina-db.el | 6 +++--- tools/gallina-syntax.el | 14 +++++++------- tools/gallina.el | 8 ++++---- 4 files changed, 15 insertions(+), 15 deletions(-) (limited to 'tools') 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 ;; 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 -;; 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 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