aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-12-31 15:23:35 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-12-31 15:23:35 +0100
commit40a248f2007e7239ce01824a18f48fb0ab7d6d22 (patch)
tree67db985d80dc3f3c3a774085098ff8c7e41097a9 /coq
parentbfdb02859bcef664b5916849f88e1ab854696f64 (diff)
comment and readme.
Diffstat (limited to 'coq')
-rw-r--r--coq/README2
-rw-r--r--coq/coq.el11
2 files changed, 7 insertions, 6 deletions
diff --git a/coq/README b/coq/README
index ab726433..9795e72a 100644
--- a/coq/README
+++ b/coq/README
@@ -6,7 +6,7 @@ Later contributions by Patrick Loiseleur, Pierre Courtieu,
Status: supported
Maintainer: Pierre Courtieu
-Coq version: 8.3
+Coq version: 8.5
Coq homepage: http://coq.inria.fr/
===========================================================================
diff --git a/coq/coq.el b/coq/coq.el
index 69c81194..3ce94e7c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -33,11 +33,12 @@
(require 'proof)
(require 'coq-system) ; load path, option, project file etc.
-(require 'coq-syntax)
-(require 'coq-local-vars)
-(require 'coq-abbrev) ; abbrev and coq specific menu
-(require 'coq-seq-compile) ; sequential compilation
-(require 'coq-par-compile) ; parallel compilation
+(require 'coq-syntax) ; font-lock, syntax categories (tactics, commands etc)
+(require 'coq-local-vars) ; setting coq args via file variables
+ ; (prefer _CoqProject file instead)
+(require 'coq-abbrev) ; abbrev and coq specific menu
+(require 'coq-seq-compile) ; sequential compilation of Requires
+(require 'coq-par-compile) ; parallel compilation of Requires
;; for compilation in Emacs < 23.3 (NB: declare function only works at top level)