Vincent Siles, Jan 2010:

Tested with the trunk version of Coq, it may not compile with v8.2
due to syntax changes.

Please edit the Makefile to point to the right version of coqc


CHANGES, Avril 2010:
Simplification of Ts_Shape lemma: the whole result was not
totally needed so it has been replaced by a weaker result
weak_type_shape for the sake of simplicity.

See glue_old.v for the full Ts_Shape lemma.