fixing a bug introduced lately (coq-save-command-p *needs* two args

beacause proof-save-command-p needs is so defined).

2 files changed, 3 insertions, 3 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 5a21cc2d..33656248 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -416,7 +416,7 @@ is moved at the end of the match if found, at LIM otherwise."
 
    ;; we are at an end command -> one ident left
    ;; FIX: we should count the number of closing item on the line
-   ((coq-save-command-p (or (coq-command-at-point) "")) 
+   ((coq-save-command-p nil (or (coq-command-at-point) "")) 
     (- proof-indent))
 
 
@@ -426,7 +426,7 @@ is moved at the end of the match if found, at LIM otherwise."
          (or (and;;"Proof ..." is a proof start (but not really a goal command)
               ;;  unless followed by a term (catch by coq-save-command-p above
               (proof-looking-at-safe "\\<Proof\\>")
-              (not (coq-save-command-p (coq-command-at-point))))
+              (not (coq-save-command-p nil (coq-command-at-point))))
              (coq-indent-goal-command-p (coq-command-at-point))
              ))
     proof-indent)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 455841d8..5d86b123 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -627,7 +627,7 @@ Used by `coq-goal-command-p'"
   (append coq-keywords-save-strict '("Proof"))
 )
 
-(defun coq-save-command-p (str)
+(defun coq-save-command-p (span str)
   "Decide whether argument is a Save command or not"
   (or (proof-string-match coq-save-command-regexp-strict str)
       (and (proof-string-match "\\`Proof\\>" str)