Verification of Redecoration for Infinite Triangular Matrices using Coinduction

The following code is additional material to the article of the same name by the authors.

Coq code for version 8.4 of Coq
Coq code for version 8.3 of Coq
List of correspondence between the symbols in the paper with the identifiers in the Coq sources

The 8.3 version runs at least under 8.3pl4. Last update June 8, 2012.
The 8.4 version differs only by some symbols reensuring compilation. Last update December 5, 2012.
Celia Picard and Ralph Matthes

Celia Picard