From c84fed036fd233454c1024f2744de0383e6e37c3 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sun, 22 Feb 2015 02:56:40 +0100
Subject: [PATCH] Typo in statement of lift_pure_step.

---
 iris_meta.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_meta.v b/iris_meta.v
index 7bb4d79d7..effbc8582 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -362,7 +362,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
     Qed.
 
     Program Definition plugExpr safe m φ P Q: expr -n> Props :=
-      n[(fun e => (lift_ePred φ e) ∨ (ht safe m P e Q))].
+      n[(fun e' => (lift_ePred φ e') → (ht safe m P e' Q))].
     Next Obligation.
       intros e1 e2 Heq w n' r HLt.
       destruct n as [|n]; [now inversion HLt | simpl in *].
-- 
GitLab