fixed some small bugs in coq indentation smie code.

1 files changed, 51 insertions, 0 deletions

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.
+
+