From 6faf6cad4f5eb9e1a7635f7119853f810217548e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 13 May 2019 15:45:06 +0200
Subject: [PATCH] un-foobar the par.v example

---
 theories/examples/par.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/examples/par.v b/theories/examples/par.v
index 14aef3b..b23b34e 100644
--- a/theories/examples/par.v
+++ b/theories/examples/par.v
@@ -1,3 +1,4 @@
+(** THIS EXAMPLE IS WIP *)
 From iris.algebra Require Import excl.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib Require Export spawn par.
@@ -100,7 +101,7 @@ Section rules.
     repeat rel_pure_r.
     tp_rec i. simpl.
     rel_rec_l. repeat rel_pure_l.
-    rewrite {3}refines_eq /refines_def. iIntros (LL) "_". clear LL.
+    rewrite {3}refines_eq /refines_def. iIntros (ρ) "#Hρ".
     iIntros (j K) "Hj". iModIntro.
     tp_bind j e2.
     pose (C:=(AppRCtx (λ: "v2", let: "v1" := join #c2 in ("v1", "v2")) :: K)).
@@ -150,7 +151,7 @@ Section rules.
     { simpl. eauto. }
     repeat rel_pure_r.
     tp_rec i. simpl.
-    rewrite {3}refines_eq /refines_def. iIntros (LL) "_". clear LL.
+    rewrite {3}refines_eq /refines_def. iIntros (ρ) "#Hρ".
     iIntros (j K) "Hj". iModIntro.
     tp_bind j e2. tp_bind i e1.
     (* execute e1 *)
-- 
GitLab