aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-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)