summaryrefslogtreecommitdiff
path: root/plugins/dp/TODO
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/dp/TODO')
-rw-r--r--plugins/dp/TODO24
1 files changed, 0 insertions, 24 deletions
diff --git a/plugins/dp/TODO b/plugins/dp/TODO
deleted file mode 100644
index 44349e21..00000000
--- a/plugins/dp/TODO
+++ /dev/null
@@ -1,24 +0,0 @@
-
-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
-----
-
-