From 5627f72c5c6824fe343b23f2bff1d91fb8fec034 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Jun 2009 11:14:48 +0000
Subject: [PATCH] added TODO list

---
 helm/software/matita/dist/TODO | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 helm/software/matita/dist/TODO

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
-- 
2.39.2