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.
Skills: Some understanding of Coq implementation, co-operation with the Coq developers to get any Coq modifications (if any) incorporated. Minimal Emacs Lisp knowledge.
Proposer: David Aspinall.