Hacking around with A Unified View of Modalities in Type Systems by Abel and Bernardy.

This code was written in an afternoon for fun and is probably broken and wrong, don't use it for anything real.

• Maps.v is Maps from Software Foundations.
• UVM.v is the core syntax and type system.
• ExXXX.v's are example instantiations of the framework.