From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Jun 2009 11:14:48 +0000 (+0000)
Subject: added TODO list
X-Git-Tag: make_still_working~3870
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5627f72c5c6824fe343b23f2bff1d91fb8fec034;p=helm.git

added TODO list
---

diff --git a/helm/software/matita/dist/TODO b/helm/software/matita/dist/TODO
new file mode 100644
index 000000000..3cc91c486
--- /dev/null
+++ b/helm/software/matita/dist/TODO
@@ -0,0 +1,20 @@
+TODO:
+- "ncoercion" statement:
+  - type processing to identify source/target
+  - transitive closure (in the new Cic)
+  - generation of hints to implement the pullback
+- principles generation:
+  - pretty printer for new statements required
+- dependency graphs
+- queries (on the trie?)
+- serialization/undo
+  - objects
+  - ng_status (moo/lexicon)
+- Tactics:
+  - satuation
+  - destruct
+
+- Library.copy_at_level
+- NCicRefiner.typeof e inferenza universi
+- hints:
+  - compare with the paper