- support Grab Existential Variables for Prooftree

- protocol change, but stay at version 3

1 files changed, 7 insertions, 0 deletions

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