1 files changed, 24 insertions, 0 deletions
diff --git a/plugins/dp/TODO b/plugins/dp/TODO
new file mode 100644
index 00000000..44349e21
--- /dev/null
+++ b/plugins/dp/TODO
@@ -0,0 +1,24 @@
+
+TODO
+----
+
+- axiomes pour les prédicats récursifs comme
+
+  Fixpoint even (n:nat) : Prop :=
+  match n with 
+  O => True
+  | S O => False
+  | S (S p) => even p
+  end.
+
+  ou encore In sur les listes du module Coq List.
+
+- discriminate
+
+- inversion (Set et Prop)
+
+
+BUGS
+----
+
+