camp coq update

[Ian Lynagh]

Hi all,

Camp coq update:

Florent Becker and I are converging on the way to structure coq proofs,
the datatypes, etc. I've also interleaved the coq definitions, proofs
etc with the LaTeX paper, in
    darcs get http://code.haskell.org/camp/devel/paper/
The .v files are understood directly by coq, while running "make" turns
them into .tex file that latex understands, with the coq displayed in
green boxes.

Many of the easier proofs, lifting {axioms on unnamed patches} into
{lemmas on named patches}, are done.

Starting on the more meaty proofs, I'm currently stuck on the "Foo"
sub-lemma, heading towards Lemma 10.1 (commute-in-sequence-consistent).
I think it should be quite easy once I work out the trick.


Thanks
Ian