diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-22 15:32:48 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-22 15:32:48 +0000 |
| commit | 204342f620cb85421981dec27d36bf76565d8db9 (patch) | |
| tree | fba7d9eaf1a2fad2394eda82b9df3321dfcb716c /coq/todo | |
| parent | 9753741c3e389e39d7df416b70e0ac40f47685a9 (diff) | |
Updated todo's.
Diffstat (limited to 'coq/todo')
| -rw-r--r-- | coq/todo | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -32,7 +32,9 @@ See also ../todo for generic things to do, priority codes. ** B Proof-by-Pointing [2 weeks] 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 (Pierre?) + We need a Coq hacker to do this. + Perhaps for new version of Coq. + da: I have old version of code sent to my by Healf. ** C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? |