From fc8e7e871912333bd885985963a1f3a96ee69ade Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 7 May 2021 13:49:52 +0200
Subject: [PATCH] Scopes for bi_car, and Remove some now implied %I
Robbert pointed out this should fix the scopes for derived_laws.
---
iris/bi/interface.v | 17 +++++++++--------
1 file changed, 9 insertions(+), 8 deletions(-)
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 70fe83bd7..a6c66ad0b 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -182,6 +182,7 @@ Structure bi := Bi {
bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
bi_forall bi_exist bi_sep bi_persistently bi_later;
}.
+Bind Scope bi_scope with bi_car.
Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.
@@ -204,18 +205,18 @@ Global Instance: Params (@bi_later) 1 := {}.
Global Arguments bi_car : simpl never.
Global Arguments bi_dist : simpl never.
Global Arguments bi_equiv : simpl never.
-Global Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_entails {PROP} _ _ : simpl never, rename.
Global Arguments bi_emp {PROP} : simpl never, rename.
Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
-Global Arguments bi_and {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_or {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
+Global Arguments bi_and {PROP} _ _ : simpl never, rename.
+Global Arguments bi_or {PROP} _ _ : simpl never, rename.
+Global Arguments bi_impl {PROP} _ _ : simpl never, rename.
Global Arguments bi_forall {PROP _} _%I : simpl never, rename.
Global Arguments bi_exist {PROP _} _%I : simpl never, rename.
-Global Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_persistently {PROP} _%I : simpl never, rename.
-Global Arguments bi_later {PROP} _%I : simpl never, rename.
+Global Arguments bi_sep {PROP} _ _ : simpl never, rename.
+Global Arguments bi_wand {PROP} _ _ : simpl never, rename.
+Global Arguments bi_persistently {PROP} _ : simpl never, rename.
+Global Arguments bi_later {PROP} _ : simpl never, rename.
Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
--
GitLab