From 04a54e2c5b6be7552a6a49abb88fa36c8de45fbe Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 20 Dec 2016 12:37:34 +0100
Subject: [PATCH] wp_app: remove commented-out tactics

---
 theories/lang/derived.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index a5947bf6..40ea3607 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -33,9 +33,7 @@ Proof.
   rewrite big_sepL_app. iDestruct "Hel" as "[Hvl Hel]".
   iAssert ([∗ list] y ∈ [], Q y)%I with "[Hvl]" as "Hvl".
   { by rewrite big_sepL_nil. }
-  (*assert (length ((of_val <$> ([] : list val)) ++ el) = length el) as Hlen by reflexivity.*)
-  remember [] as vl. clear Heqvl. (*remember (length el) as n. clear Heqn.*)
-  iInduction el as [|e el] "IH" forall (vl).
+  remember [] as vl. clear Heqvl. iInduction el as [|e el] "IH" forall (vl).
   - rewrite app_nil_r. by iApply "HΦ".
   - destruct Hf as [vf Hf]. set (K := AppRCtx vf vl el).
     rewrite (_ : App f ((of_val <$> vl) ++ e :: el) = fill_item K e); last first.
-- 
GitLab