From 984b5935e5dc97eb9cf1e10dbffbadab8e21fc83 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 18 Mar 2019 13:44:39 +0100
Subject: [PATCH] remove Undo's

---
 theories/tests/proofmode_tests.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index 1adc17e..04bfb10 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -13,8 +13,6 @@ Lemma test1 A P t :
   REL (#2 + #2) << (λ: <>, t) #() : A.
 Proof.
   iIntros "HP Ht".
-  rel_bind_l #2. Undo.
-  rel_pure_l (_ + _)%E. Undo.
   rel_pure_l. repeat rel_pure_r.
   by iApply "Ht".
 Qed.
-- 
GitLab