blob: 366feb7c9649eb3b15f30e0a48107b67f7cfa48d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
<h2>Proof-by-pointing support for Coq</h2>
<p>
Coq already has sophisticated notions of proof-by-pointing,
and old work on support for Proof General may be helpful.
We want to integrate with the latest version of Coq's
proof-by-pointing, possibly improving Proof General's
support along the way.
</p>
<p>
<b>Skills:</b>
Some understanding of Coq implementation, co-operation with
the Coq developers to get any Coq modifications (if any) incorporated.
Minimal Emacs Lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
|
