Awesome

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: