From 88343f978a0e09f1673ccec228fc7ab9c98d46e7 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Thu, 17 Jan 2013 07:47:37 +0000
Subject: - support Grab Existential Variables for Prooftree - protocol change,
 but stay at version 3

---
 coq/coq.el | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index b0906f65..451a1762 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -202,6 +202,12 @@ See also `coq-hide-additional-subgoals'."
   :type 'regexp
   :group 'coq-proof-tree)
 
+(defcustom coq-proof-tree-new-layer-command-regexp
+  "^\\(\\(Proof\\)\\|\\(Grab Existential Variables\\)\\)"
+  "Regexp for `proof-tree-new-layer-command-regexp'."
+  :type 'regexp
+  :group 'coq-proof-tree)
+
 (defcustom coq-proof-tree-current-goal-regexp
   (concat "^[0-9]+ \\(?:focused \\)?subgoal\\(?:s\\)?"
           "\\(?: (unfocused: [-0-9]+)\\)?\\(?:\\s-*, subgoal 1\\)? "
@@ -1191,6 +1197,7 @@ flag Printing All set."
    proof-tree-ignored-commands-regexp coq-proof-tree-ignored-commands-regexp
    proof-tree-navigation-command-regexp coq-navigation-command-regexp
    proof-tree-cheating-regexp coq-proof-tree-cheating-regexp
+   proof-tree-new-layer-command-regexp coq-proof-tree-new-layer-command-regexp
    proof-tree-current-goal-regexp coq-proof-tree-current-goal-regexp
    proof-tree-update-goal-regexp coq-proof-tree-update-goal-regexp
    proof-tree-existential-regexp coq-proof-tree-existential-regexp
-- 
cgit v1.2.3