Merged requested to merge ralf/intuitionistically into gen_proofmode
I am very unsure about the instances in
class_instances.v -- both about what I added (necessary to make it all compile again), and about what else I should add because the modality commutes with various things.
This will break reverse dependencies if they relied on "intuitionitsically" to be syntactically equal (and not just convertible) to "affinely persistently".
Fixes #126 (closed)