diff options
| author | Hendrik Tews | 2012-01-04 20:43:04 +0000 |
|---|---|---|
| committer | Hendrik Tews | 2012-01-04 20:43:04 +0000 |
| commit | 83752f800e51f6945a8043a98cdbee732f63d982 (patch) | |
| tree | 6e951a3cb2f875a9c0801dc3fe4c2a06c8557574 /coq | |
| parent | b6cc4c3ce79afa83f5293559d334148787f64ecf (diff) | |
* fix case where some existential is instantiated with the last proof command
* protocol change
- rename proof-complete into proof-finished and add existential info
- add proof-complete message
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -259,9 +259,9 @@ A setting of nil means show all output from Coq. See also :type 'regexp :group 'coq-proof-tree) -(defcustom coq-proof-tree-proof-completed-regexp +(defcustom coq-proof-tree-proof-finished-regexp "^\\(?:Proof completed\\)\\|\\(?:No more subgoals\\)\\." - "Regexp for `proof-tree-proof-completed-regexp'." + "Regexp for `proof-tree-proof-finished-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -1330,7 +1330,7 @@ This is specific to `coq-mode'." coq-proof-tree-existentials-state-end-regexp proof-tree-additional-subgoal-ID-regexp coq-proof-tree-additional-subgoal-ID-regexp - proof-tree-proof-completed-regexp coq-proof-tree-proof-completed-regexp + proof-tree-proof-finished-regexp coq-proof-tree-proof-finished-regexp proof-tree-extract-instantiated-existentials 'coq-extract-instantiated-existentials proof-tree-show-sequent-command 'coq-show-sequent-command |