Add some missing modes

Merged Paolo G. Giarrusso requested to merge Blaisorblade/iris:more-modes into master
  • Add modes missing from stdpp's base.v, except for sets (and maps).
  • Add most missing modes from ofe.v and cmra.v

I expect landing this to not be trivial, so let me encourage cherry-picking and work-stealing from the outset.

UPDATED: The example for Equiv lives at, on top of this MR. It seems to work but in the end we agreed to not include it.

In fact, Iris builds here with the Equiv mode with few fixes, despite the bug @robbertkrebbers identified, so I added the extra commits.

Edited by Paolo G. Giarrusso

Merge request reports