Added the keyword "Local :=" to the coq-goal-command-p function, like

Definition.

1 files changed, 1 insertions, 0 deletions

diff --git a/coq/coq.el b/coq/coq.el
index b9c86556..1240eda5 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -235,6 +235,7 @@
 (defun coq-goal-command-p (str)
   "Decide whether argument is a goal or not"
   (and (proof-string-match coq-goal-command-regexp str)
+       (not (proof-string-match "Local.*:=" str))
        (not (proof-string-match "Definition.*:=" str))
        (not (proof-string-match "Module.*:=" str))
        (not (proof-string-match "Declare Module.*:" str)) ;neither : or :=