aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/gallina-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2013-12-17 18:26:48 +0100
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2013-12-17 18:27:02 +0100
commit30b58d43e48569afb50a35d3915ec7d453a61f5d (patch)
tree246891f764f24fe704fe9bb8a093da91adf788a1 /tools/gallina-syntax.el
parent5080f91a191aa08bf29790addb5b8614ba8323a8 (diff)
Attempt to adapt .el files too. doc/refman/RefMan-uti.tex has still to be fixed.
Diffstat (limited to 'tools/gallina-syntax.el')
-rw-r--r--tools/gallina-syntax.el14
1 files changed, 7 insertions, 7 deletions
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 ***