From 4bce74dd1e4682086b9497ad3577c88b4a01df0c Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Wed, 12 Sep 2012 12:33:13 +0000
Subject: treat #450 by requiring that proofs are started with Proof

---
 coq/coq.el            | 8 +++++++-
 doc/ProofGeneral.texi | 6 ++++++
 generic/proof-tree.el | 7 +++++--
 3 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index ceb81311..d260ef48 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -199,8 +199,14 @@ See also `coq-hide-additional-subgoals'."
   :group 'coq-config
   :package-version '(ProofGeneral . "4.2"))
 
+;; Ignore all commands that start a proof. Otherwise "Proof" will appear
+;; as superfluous node in the proof tree. Note that we cannot ignore Proof,
+;; because, Fixpoint does not display the proof goal, see Coq bug #2776. 
 (defcustom coq-proof-tree-ignored-commands-regexp
-  "^\\(Show\\)\\|\\(Locate\\)"
+  (concat "^\\(\\(Show\\)\\|\\(Locate\\)\\|"
+          "\\(Theorem\\)\\|\\(Lemma\\)\\|\\(Remark\\)\\|\\(Fact\\)\\|"
+          "\\(Corollary\\)\\|\\(Proposition\\)\\|\\(Definition\\)\\|"
+          "\\(Let\\)\\|\\(Fixpoint\\)\\|\\(CoFixpoint\\)\\)")
   "Regexp for `proof-tree-ignored-commands-regexp'."
   :type 'regexp
   :group 'coq-proof-tree)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 3c3d4a3b..05f3d1ed 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4770,6 +4770,12 @@ Starting with Proof General version 4.2 and Coq version 8.4, Coq
 Proof General has full support for proof-tree visualization, 
 @pxref{Graphical Proof-Tree Visualization}.
 
+Proof-tree visualization does currently not support Coq's command 
+``Grab Existential Variables''.
+
+For the visualization to work properly, proofs must be started
+with ``Proof.'', which is encouraged practice anyway (see Coq Bug
+#2776).
 
 @c =================================================================
 @c
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 6a34d919..b73c2308 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -118,9 +118,12 @@
 (defcustom proof-tree-ignored-commands-regexp nil
   "Commands that should be ignored for the prooftree display.
 The output of commands matching this regular expression is not
-send to prooftree. It should match commands that display
+sent to prooftree. It should match commands that display
 additional information but do not make any proof progress. Leave
-at nil to act on all commands."
+at nil to act on all commands.
+
+For Coq this regular expression should contain all commands such
+as Lemma, that can start a proof."
   :type '(choice regexp (const nil))
   :group 'proof-tree-internals)
 
-- 
cgit v1.2.3