diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:01:07 +0200 |
| commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
| tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /plugins/dp/TODO | |
| parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
| parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) | |
Merge branch 'experimental/master'
Diffstat (limited to 'plugins/dp/TODO')
| -rw-r--r-- | plugins/dp/TODO | 24 |
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 ----- - - |