From bdc654514b5c30eb0a2d3b8e6903a5d4e9fc6953 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 12:46:40 +0100
Subject: [PATCH] Make sure derived lemmas do not peek into the model.

---
 iris/lifting.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/lifting.v b/iris/lifting.v
index c63c9cb55..eff6ff6fa 100644
--- a/iris/lifting.v
+++ b/iris/lifting.v
@@ -1,7 +1,5 @@
 Require Export iris.weakestpre.
 Require Import iris.wsat.
-Import uPred.
-
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
@@ -55,6 +53,8 @@ Proof.
 Qed.
 
 (** Derived lifting lemmas. *)
+Opaque uPred_holds.
+Import uPred.
 Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
   to_val e1 = None →
   reducible e1 σ1 →
-- 
GitLab