From ae972c48eb11f44ceea7666c7d8868701535beff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jan 2016 09:49:18 +0100
Subject: [PATCH] Make uPred_holds Opaque so we do not accidentally go into the
 model.

---
 iris/lifting.v     | 1 +
 iris/pviewshifts.v | 1 +
 iris/weakestpre.v  | 1 +
 modures/logic.v    | 2 ++
 4 files changed, 5 insertions(+)

diff --git a/iris/lifting.v b/iris/lifting.v
index 7e36e3913..8526f16e4 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -11,6 +11,7 @@ Context {Σ : iParam}.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
 Implicit Types σ : istate Σ.
+Transparent uPred_holds.
 
 Lemma wp_lift_step E1 E2
     (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) Q e1 σ1 :
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index ced05a0cb..2e83581e4 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -30,6 +30,7 @@ Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
 Implicit Types m : icmra' Σ.
+Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
 Proof.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index 15bb4639e..3e34864fa 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -58,6 +58,7 @@ Implicit Types P : iProp Σ.
 Implicit Types Q : ival Σ → iProp Σ.
 Implicit Types v : ival Σ.
 Implicit Types e : iexpr Σ.
+Transparent uPred_holds.
 
 Lemma wp_weaken E1 E2 e Q1 Q2 r n n' :
   E1 ⊆ E2 → (∀ v r n', n' ≤ n → ✓{n'} r → Q1 v n' r → Q2 v n' r) →
diff --git a/modures/logic.v b/modures/logic.v
index dcab3b504..e9b058004 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -11,6 +11,8 @@ 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.
 Hint Resolve uPred_0.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
-- 
GitLab