This is a list of things which need doing to the lego mode.

* Fixing up errors caused by pbp-generated commands.

* undo support for LEGO needs to consider Discharge; perhaps unrol to
  the beginning of the module?

* pbp code doesn't quite accord with the tech report; in particular it
  decodes annotations eagerly. Lazily would be faster, and it's what
  the tech report claims
  --- djs: probably not much faster, actually.

* It would be nice to have a version ported to emacs19 (or
  20). Unfortunately, it's currently impossible to port the pbp code,
  since emacs19 doesn't properly handle highlighting of nested
  overlays. The bulk of the stuff dependent on which version of emacs
  is running has been moved to proof-dependencies.el, but there are
  doubtless differences in font-locking and menu code which will
  require some work.

* file handling could be more robust

* LEGO mode might incorporate changes to Coq mode menu, in particular
  making help refer to the info file.

* LEGO and Coq modes overwrite each other.

* We need to go over to piped communication rather than ptys to fix the
  ^G bug. In this circumstance there's a bug in the eager annotation
  code

Here are things to be done to Coq mode:

* Restart if going back to beginning of proof.

* C-c u inside a Section should reset the whole section, then redo defns

* There's a bug so the goal buffer isn't displaying everything that
  happens.

* Sections and files are handled incorrectly.

* Update documentation to include C-c C-s.