diff options
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
2 files changed, 8 insertions, 1 deletions
@@ -30,7 +30,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Support for bullets, braces and Grab Existential Variables for Prooftree. -*** Suuport for _Coqproject files +*** Support for _Coqproject files According to Coq documentation, it is advised to use coq_makefile -f _CoqProject -o Makefile to build your Makefile automatically @@ -46,6 +46,11 @@ 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. + * Changes of Proof General 4.2 from Proof General 4.1 ** Generic/misc changes @@ -26,6 +26,8 @@ (defvar string nil) ; dynamic scope in coq-insert-as stuff (defvar coq-auto-insert-as nil) ; defpacustom (defvar coq-time-commands nil) ; defpacustom + (defvar use-project-file t) ; defpacustom + (defvar coq-project-filename nil) ; defpacustom (defvar coq-use-editing-holes nil) ; defpacustom (defvar coq-hide-additional-subgoals nil) ; defpacustom (proof-ready-for-assistant 'coq)) ; compile for coq |