This repository is no longer maintained. The proofs have been moved to a coq-community project for long-term maintenance.
Web appendix accompanying the paper:
Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
To build the theory files you need:
mathcomp-1.6.4 coq-8.7 (coq-8.6 and mathcomp-1.6.1 should work as well)
To build the HTML documentation run "make website". The entry points to the two developments will then be gernerated in
website/[C]PDL/toc.html