Merge branch 'ralf/monpred-scope' into 'master'

fix monPred scope binding See merge request iris/iris!638

Merge branch 'ralf/monpred-scope' into 'master'
fix monPred scope binding See merge request iris/iris!638
842fb394 · Robbert Krebbers · d8ec293d · aff8e8a3 · 842fb394
Commit 842fb394 authored 4 years ago by Robbert Krebbers
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -27,8 +27,7 @@ Record monPred :=
            monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
 Local Existing Instance monPred_mono.
-Declare Scope monPred.
+Bind Scope bi_scope with monPred.
-Bind Scope monPred with bi.
 Implicit Types P Q : monPred.