root
- src
- tex
- Makefile
- README
- catch_commute.tex
- catch_merge.tex
- catch_more_bits.tex
- definitions.tex
- dvipsnam.mp
- grafbase.mf
- grafbase.mp
- mathlig.tex
- mathtools.sty
- mfpic.sty
- mfpic.tex
- mfppatch.tex
- mhsetup.sty
- named_patch_motivation.tex
- overview.tex
- patch_merge.tex
- preamble.tex
- preamble_mfpic.tex
- sensible_unnamed_patch_sequences.tex
- theory.tex
To run the proofs or build the docs, you need up-to-date coq and coqdoc.
I am currently using v8.3 (13693).