From df8431507b75d58bbfe3c11c92b029dfbaf313e3 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 31 Jan 2019 13:02:13 +0100
Subject: [PATCH] move is_closed_expr' to model.v

---
 theories/logic/model.v | 12 ++++++++----
 theories/logic/rules.v |  3 ---
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/theories/logic/model.v b/theories/logic/model.v
index 37a2675..e10eacd 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -336,18 +336,22 @@ Section related_facts.
 
 End related_facts.
 
+(** TODO this is a terrible hack and I should be ashamed of myself.
+    See iris issue 225. *)
+Notation is_closed_expr' := (λ e, ∀ vs, subst_map vs e = e).
+
 Section monadic.
   Context `{relocG Σ}.
 
   Lemma refines_ret' E Γ e1 e2 A :
-    is_closed_expr [] e1 →
-    is_closed_expr [] e2 →
+    is_closed_expr' e1 →
+    is_closed_expr' e2 →
     interp_expr E e1 e2 A -∗ {E;Γ} ⊨ e1 << e2 : A.
   Proof.
-    iIntros (??) "HA".
+    iIntros (Hcl1 Hcl2) "HA".
     rewrite refines_eq /refines_def.
     iIntros (vvs ρ) "#Hs #HΓ".
-    rewrite !subst_map_is_closed_nil//.
+    by rewrite Hcl1 Hcl2.
   Qed.
 
   Lemma refines_bind K K' E Γ A A' e e' :
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index c1b53ce..c6e7265 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -74,9 +74,6 @@ Section rules.
     by rewrite subst_map_fill.
   Qed.
 
-  (* See iris issue 225 *)
-  Notation is_closed_expr' := (λ e, ∀ vs, subst_map vs e = e).
-
   Lemma refines_wp_l Γ K e1 e2 A :
     is_closed_expr' e1 →
     (WP e1 {{ v,
-- 
GitLab