From a2007818ad381dad0f489cbea8817df401e57c9f Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Thu, 10 Nov 2011 12:12:32 +0000
Subject: fixed some small bugs in coq indentation smie code.

---
 coq/TODO | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 coq/TODO

(limited to 'coq/TODO')

diff --git a/coq/TODO b/coq/TODO
new file mode 100644
index 00000000..09140d77
--- /dev/null
+++ b/coq/TODO
@@ -0,0 +1,51 @@
+-*- outline -*-  
+
+** important: deal with different levels of the "in" keyword
+
+let x := y in      : expression
+eval x in y        : commande
+unfold x in y      : tactique
+
+
+** important: Have an option for indenting style:
+
+Current behavior:
+
+Lemma foo: forall x,
+            f x = 0.
+
+and: 
+
+functionfoo bar1 bar2
+    	    bar3
+
+
+Commonly used behavior:
+
+Lemma foo: forall x,
+  f x = 0.
+
+and
+
+functionfoo bar1 bar2
+  bar3
+
+
+** (less important) Indent correctly this:
+
+Proof with auto.
+           intro.
+
+instead of:
+
+Proof with auto.
+  intro.
+
+
+Workaroud for the moment, write the script like this:
+
+Proof with
+  auto.
+  intro.
+
+
-- 
cgit v1.2.3