diff options
Diffstat (limited to 'html/projects/coqpbp.html')
| -rw-r--r-- | html/projects/coqpbp.html | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/html/projects/coqpbp.html b/html/projects/coqpbp.html new file mode 100644 index 00000000..366feb7c --- /dev/null +++ b/html/projects/coqpbp.html @@ -0,0 +1,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> |