Cleaned TODO file in coq/.

1 files changed, 18 insertions, 29 deletions

diff --git a/coq/TODO b/coq/TODO
index ba8b310e..c503dc24 100644
--- a/coq/TODO
+++ b/coq/TODO
@@ -7,47 +7,36 @@ eval x in y        : commande
 unfold x in y      : tactique
 
 
-** important: Have an option for indenting style:
+** important: fix indention of definitions:
 
 Current behavior:
 
-Lemma foo: forall x,
-            f x = 0.
+function foo bar1 bar2
+    	 bar3
 
-and: 
+Should be
 
-functionfoo bar1 bar2
-    	    bar3
+function foo bar1 bar2
+  <>bar3
+(<> length parameterized by coq-smie-after-bolp-indentation)
+or
 
+function foo bar1 bar2
+             bar3
 
-Commonly used behavior:
+depending on an option (coq-indent-box-style).
 
-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.
+** Fix indentation of ;
 
+Current behavior:
 
-Workaroud for the moment, write the script like this:
+idtac ;
+  idtac.
 
-Proof with
-  auto.
-  intro.
+but:
 
+idtac; idtac;
+idtac.
 
 ** dealing with several project files.