* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.

(coq-smie-backward-token): Don't burp at EOB.
(coq-smie-rules): Indent top-level ":" like ":=".

4 files changed, 35 insertions, 12 deletions

diff --git a/CHANGES b/CHANGES
index 7a1d34b1..bac19211 100644
--- a/CHANGES
+++ b/CHANGES
@@ -51,6 +51,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
     Should work for induction and destruct for now. Toggle this option
     with Coq/Settings/Auto insert As.
 
+*** Support for prettify-symbols-mode.
+
 * Changes of Proof General 4.2 from Proof General 4.1
 
 ** Generic/misc changes
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index e9dd02fb..fd1284f8 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -77,8 +77,7 @@ But in
 
 intros.      or        Proof foo.
 
-the token of \".\" is simply \".\".
-"
+the token of \".\" is simply \".\"."
   (save-excursion
     (let ((p (point)) (beg (coq-find-real-start))) ; moves to real start of command
       (cond
@@ -91,8 +90,17 @@ the token of \".\" is simply \".\".
 	    (coq-smie-detect-goal-command))
 	(save-excursion
 	  (goto-char (+ p 1))
-	  (if (equal (smie-default-forward-token) "Proof")
-	      "." ". proofstart")))
+          (let ((tok (smie-default-forward-token)))
+            (cond
+             ;; If the next token is "Proof", then the current command does
+             ;; introduce a proof, but the user opted to use the explicit
+             ;; "Proof" command, so the current command doesn't itself start
+             ;; the proof.
+             ((equal tok "Proof") ".")
+             ;; If the next command is a new definition, then the current
+             ;; command didn't actually start a proof!
+             ((member tok '("Let" "Definition" "Inductive" "Fixpoint")) ".")
+             (t ". proofstart")))))
        ((equal (coq-smie-module-deambiguate) "Module start")
 	". modulestart")
        (t ".")))))
@@ -554,7 +562,7 @@ The point should be at the beginning of the command name."
       ;; qualifier.
       (let ((nxtnxt (char-after (+ (point) (length tok)))))
 	(if (eq nxtnxt ?\() ". selector"
-	  (if (eq (char-syntax nxtnxt) ?\ )
+	  (if (or (null nxtnxt) (eq (char-syntax nxtnxt) ?\ ))
 	      ;; command terminator: ". proofstart" et al
 	      (save-excursion (forward-char (- (length tok) 1))
 			      (coq-smie-.-deambiguate))
@@ -805,12 +813,15 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
 	(save-excursion (coq-find-real-start)
 			`(column . ,(current-column))))
 
-       ((member token '(":= module" ":= inductive" ":= def"))
-	(if (smie-rule-hanging-p)
-	    (save-excursion (coq-find-real-start)
-			    `(column . ,(current-column)))
-	  (save-excursion (coq-find-real-start)
-			  `(column . ,(+ 2 (current-column))))))
+       ((or (member token '(":= module" ":= inductive" ":= def"))
+            (and (equal token ":") (smie-rule-parent-p ".")))
+        (let ((pcol
+               (save-excursion
+                 ;; Indent relative to the beginning of the current command
+                 ;; rather than relative to the previous command.
+                 (smie-backward-sexp token)
+                 (current-column))))
+          `(column . ,(if (smie-rule-hanging-p) pcol (+ 2 pcol)))))
 
        ((equal token "|")
 	(cond ((smie-rule-parent-p "with match")
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index b524d956..c452cd1b 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -21,6 +21,16 @@ Record a : Type := make_a {
      | C2 : forall n, test n
      | C3 : forall n, test n
      | C4 : forall n, test n.
+
+  Let x : = 1.  Let y := 2.
+                
+  Let y := (1, 2, 3,
+            4, 5).
+  
+    Inductive test3             (* fixindent *)
+      : nat -> Prop
+      := C1 : forall n, test n
+       | C2 : forall n, test n
 }
 
 Lemma toto:nat.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index cc7e56f8..a8e79fcd 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -863,7 +863,7 @@ used in `proof-add-to-queue' when we start processing a queue, and in
 
       ;; Replace CRs from string with spaces to avoid spurious prompts.
       (if proof-shell-strip-crs-from-input
-	  (setq string (subst-char-in-string ?\n ?\  string t)))
+	  (setq string (subst-char-in-string ?\n ?\  string)))
 
       (insert string)