From 1c0b0d32f95d7555943ab86a2de6666e39e84c13 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Wed, 4 Jun 2014 12:22:43 +0000 Subject: * 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 ":=". --- coq/ex/indent.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'coq/ex') 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. -- cgit v1.2.3