Readme for Coq development to be included with Paper:

A Formalisation of Weak Normalisation
 (with respect to Permutations)
 of Sequent Calculus Proofs.

published in the LMS Journal of Computation and Mathematics

The system required is the release version of Coq V6.1 (Dec 24 1996).

The Makefile is a standard one produced by the coqdep utility supplied
with the system, and provided the COQTOP and COQBIN environment variables
are correctly specified for your installation, you should have no trouble
compiling the files. In order to manually run through any of the later
proofs earlier files must have been compiled. It is recommended that
you compile everything (using make all) before trying to load any file.

Andrew A Adams 13/1/00.
 (aaa@cs.st-and.ac.uk)