Merged 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
PROPargument at level 200.
If we want to do this, I suggest we apply this to all similar notations in std++ and Iris too.