Theory files 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 or mathcomp-1.7.0 coq-8.9 (coq-8.8 or coq-8.7 should work as well)
To build the HTML documentation run "make html". The entry points to the two developments will then be generated in
html/toc.html
The documentation can also be browsed online at: