From 8a97c25f512362bec65a11389717584ff70d5836 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Jun 2018 10:43:18 +0200
Subject: [PATCH] be more explicit about instance scope; move Hint to the lemma
it uses
---
theories/base_logic/bi.v | 11 +++++++----
theories/base_logic/derived.v | 3 ---
theories/base_logic/upred.v | 2 +-
3 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 46e434466..5483338d5 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -2,7 +2,7 @@ From iris.bi Require Export derived_connectives updates plainly.
From iris.base_logic Require Export upred.
Import uPred_primitive.
-(** BI and other MoSeL instances for uPred. This file does *not* unseal. *)
+(** BI instances for uPred. This file does *not* unseal. *)
Definition uPred_emp {M} : uPred M := uPred_pure True.
@@ -124,7 +124,7 @@ Proof.
- exact: later_plainly_1.
- exact: later_plainly_2.
Qed.
-Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
+Global Instance uPred_plainlyC M : BiPlainly (uPredSI M) :=
{| bi_plainly_mixin := uPred_plainly_mixin M |}.
Lemma uPred_bupd_mixin M : BiBUpdMixin (uPredI M) uPred_bupd.
@@ -136,15 +136,18 @@ Proof.
- exact: bupd_trans.
- exact: bupd_frame_r.
Qed.
-Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+Global Instance uPred_bi_bupd M : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
-Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
+Global Instance uPred_bi_bupd_plainly M : BiBUpdPlainly (uPredSI M).
Proof. exact: bupd_plainly. Qed.
(** extra BI instances *)
Global Instance uPred_affine : BiAffine (uPredI M) | 0.
Proof. intros P Q. exact: pure_intro. Qed.
+(* Also add this to the global hint database, otherwise [eauto] won't work for
+many lemmas that have [BiAffine] as a premise. *)
+Hint Immediate uPred_affine.
Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
Proof. exact: @plainly_exist_1. Qed.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index f4fe5135f..813c8f460 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -138,7 +138,4 @@ Global Instance uPred_ownM_sep_homomorphism :
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
End derived.
-(* Also add this to the global hint database, otherwise [eauto] won't work for
-many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate uPred_affine.
End uPred.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index a47ddc994..c09414bc8 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -348,7 +348,7 @@ Definition unseal_eqs :=
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
uPred_cmra_valid_eq, @uPred_bupd_eq).
-Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+Ltac unseal :=
rewrite !unseal_eqs /=.
Section primitive.
--
GitLab