Fix discrepancies in bi notations.

Merged Robbert Krebbers requested to merge robbert/bi_notations into master

Thanks to @Blaisorblade, based on, but applied to similar notations too.

Maybe TODO, as suggested by @Blaisorblade:

  • Put these notations at level 0 and 1.
  • Out the PROP argument at level 200.

If we want to do this, I suggest we apply this to all similar notations in std++ and Iris too.

Edited by Robbert Krebbers

Merge request reports