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.