diff options
-rw-r--r-- | CHANGES | 26 | ||||
-rw-r--r-- | coq/coq.el | 33 |
2 files changed, 33 insertions, 26 deletions
@@ -33,18 +33,29 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. Indentation supports only bullets of length <= 4 (like ----). Longer may be supported if needed. -*** by default, forall at the start of a lemma are not indented as a box - For instance, this is indented like this: +*** smie indentation is now the only choice. + Old code removed. will work only if emacs >= 23.3. + +*** indentation now supports { at end of line: + example: + + assert (h:n = k). { + apply foo. + reflexivity. } + apply h. + +*** Default indentation of forall and exists is not boxed anymore + For instance, this is now indented like this: Lemma foo: forall x y, - x = 0 -> ... . + x = 0 -> ... . (* like if forall x y, was on its own line *) instead of: Lemma foo: forall x y, x = 0 -> ... . - Put (setq coq-indent-box-style t) to bring the box style back. + do this: (setq coq-indent-box-style t) to bring the box style back. *** Support for bullets, braces and Grab Existential Variables for Prooftree. @@ -52,7 +63,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. According to Coq documentation, it is advised to use coq_makefile -f _CoqProject -o Makefile to build your Makefile automatically - from "profect file" _CoqProject. Such a file should contains the + from "profect file" _CoqProject. Such a file should contain the options to pass to coq_makefile, i.e. paths to add to coq load path (-I, -R) and other options to pass to coqc/coqtop (-arg). @@ -64,11 +75,6 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. the use of local file variables (which remains possible and overrides project file options). -*** Automatic insertion of "as" clauses. - - Should work for induction and destruct for now. Toggle this option - with Coq/Settings/Auto insert As. - *** Support for prettify-symbols-mode. * Changes of Proof General 4.2 from Proof General 4.1 @@ -1381,22 +1381,23 @@ Warning: proof-nested-undo-regexp coq-state-changing-commands-regexp proof-script-imenu-generic-expression coq-generic-expression) - (if (fboundp 'smie-setup) ; always use smie, old indentation code removed - (progn - (smie-setup coq-smie-grammar #'coq-smie-rules - :forward-token #'coq-smie-forward-token - :backward-token #'coq-smie-backward-token)) - (require 'coq-indent) - (setq - ;; indentation is implemented in coq-indent.el - indent-line-function 'coq-indent-line - proof-indent-any-regexp coq-indent-any-regexp - proof-indent-open-regexp coq-indent-open-regexp - proof-indent-close-regexp coq-indent-close-regexp) - - (make-local-variable 'indent-region-function) - (setq indent-region-function 'coq-indent-region)) - + (when (fboundp 'smie-setup) ; always use smie, old indentation code removed + (smie-setup coq-smie-grammar #'coq-smie-rules + :forward-token #'coq-smie-forward-token + :backward-token #'coq-smie-backward-token)) + + ;; old indentation code. + ;; (require 'coq-indent) + ;; (setq + ;; ;; indentation is implemented in coq-indent.el + ;; indent-line-function 'coq-indent-line + ;; proof-indent-any-regexp coq-indent-any-regexp + ;; proof-indent-open-regexp coq-indent-open-regexp + ;; proof-indent-close-regexp coq-indent-close-regexp) + ;; (make-local-variable 'indent-region-function) + ;; (setq indent-region-function 'coq-indent-region) + + ;; span menu (setq proof-script-span-context-menu-extensions 'coq-create-span-menu) |