diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 17:20:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 17:20:29 +0000 |
| commit | 3b75d8b8658495da28473c156b73c0f291b85885 (patch) | |
| tree | 18cd912518e231ce54a3d38e84bc280b9efcc20f /coq | |
| parent | 16ea2ed4c4283d23447545e50a2f93ba22225dbe (diff) | |
Updated.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/todo | 11 |
1 files changed, 10 insertions, 1 deletions
@@ -5,7 +5,16 @@ See also ../todo for generic things to do, priority codes. -** B Proof-by-Pointing [1 month] +** C Auto-compile-vos + Would be nice to ressurect this: interaction between PG + and make system is tricky and tedious. + + +** D Loss of synchronisation with silent mode + Apocryphal story, no test cases. + + +** B Proof-by-Pointing [1 month+] (2002) da: Yves Bertot told me that his CtCoq proof-by-pointing code is in the Coq kernel now, so would be useful for PG. We need a Coq hacker to do this. |