Skip to content
GitLab

Fix discrepancies in bi notations.

Merged Robbert Krebbers requested to merge robbert/bi_notations into master

Thanks to @Blaisorblade, based on https://gitlab.mpi-sws.org/Blaisorblade/iris-coq/commit/0739608d32272ca5679bf504a569b3ddd50c7b29, 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