* 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 ":=".

1 files changed, 10 insertions, 0 deletions

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.