From 6beb51d3122f757c29e7f1f5a2e8d3594ad2868f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 25 Feb 2016 14:18:35 +0100
Subject: [PATCH] stop playing tricks with uPred_holds opacitiy. We now have
 proper sealing.

---
 algebra/upred.v             | 2 --
 program_logic/lifting.v     | 2 --
 program_logic/pviewshifts.v | 2 --
 program_logic/weakestpre.v  | 2 --
 4 files changed, 8 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 4a31b059d..7fd9b5bff 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -10,8 +10,6 @@ Record uPred (M : cmraT) : Type := IProp {
     uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
 }.
 Arguments uPred_holds {_} _ _ _ : simpl never.
-Global Opaque uPred_holds.
-Local Transparent uPred_holds.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
 
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 365716b3f..0982d5242 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -14,7 +14,6 @@ Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
-Transparent uPred_holds.
 
 Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, ■ True)))%I.
 
@@ -59,7 +58,6 @@ Proof.
 Qed.
 
 (** Derived lifting lemmas. *)
-Opaque uPred_holds.
 Import uPred.
 
 Lemma wp_lift_atomic_step {E Φ} e1
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 1268b9740..c606062fa 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -43,7 +43,6 @@ Section pvs.
 Context {Λ : language} {Σ : iFunctor}.
 Implicit Types P Q : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
-Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
@@ -144,7 +143,6 @@ Proof.
 Qed.
 
 (** * Derived rules *)
-Opaque uPred_holds.
 Import uPred.
 Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index fea680774..9a0d67233 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -70,7 +70,6 @@ Implicit Types P : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Transparent uPred_holds.
 
 Global Instance wp_ne E e n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
@@ -218,7 +217,6 @@ Proof.
 Qed.
 
 (** * Derived rules *)
-Opaque uPred_holds.
 Import uPred.
 Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → || e @ E {{ Φ }} ⊑ || e @ E {{ Ψ }}.
 Proof. by apply wp_mask_frame_mono. Qed.
-- 
GitLab