]> matita.cs.unibo.it Git - helm.git/commitdiff
added TODO list
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 11:14:48 +0000 (11:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 11:14:48 +0000 (11:14 +0000)
helm/software/matita/dist/TODO [new file with mode: 0644]

diff --git a/helm/software/matita/dist/TODO b/helm/software/matita/dist/TODO
new file mode 100644 (file)
index 0000000..3cc91c4
--- /dev/null
@@ -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