This is a fork from Tadeusz Litak's formalisation of W. Ruitenburg JSL 1984 paper "On the Period of Sequences (An(p)) in Intuitionistic Propositional Calculus", for Coq v8.4pl6.

What is being developed in 8.6/ is a port that is intended to 1. be compatible with Coq v8.6, and 2. make the least sense of what is going on.