From 493d7eb902c7bb4e59d0d0de6c9632f896ecf360 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 7 Feb 2018 11:12:37 +0100
Subject: [PATCH] Fix notation scopes of `absolutely` and `relatively`.

---
 theories/bi/monpred.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 4305ae2c2..69b2d365f 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -27,6 +27,8 @@ Record monPred :=
             monPred_mono : Proper ((⊑) ==> (⊢)) monPred_at }.
 Local Existing Instance monPred_mono.
 
+Bind Scope monPred with bi.
+
 Implicit Types P Q : monPred.
 
 (** Ofe + Cofe instances  *)
@@ -207,6 +209,8 @@ Global Instance monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
 Definition monPred_bupd_eq `{BUpd PROP} : @bupd monPred _ = _ := seal_eq _.
 End Bi.
 
+Arguments monPred_absolutely {_ _} _%I.
+Arguments monPred_relatively {_ _} _%I.
 Notation "'∀ᵢ' P" := (monPred_absolutely P) (at level 20, right associativity) : bi_scope.
 Notation "'∃ᵢ' P" := (monPred_relatively P) (at level 20, right associativity) : bi_scope.
 
-- 
GitLab