From 83752f800e51f6945a8043a98cdbee732f63d982 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Wed, 4 Jan 2012 20:43:04 +0000
Subject: * 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

---
 coq/coq.el | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 286e3694..768e8c6e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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
-- 
cgit v1.2.3