From 8a675a006afd2760ef2b028f05623963f46ae33b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 23 Aug 2016 10:25:59 +0200
Subject: [PATCH] Remove old tests about heap_lang reductions.

---
 tests/heap_lang.v | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 262779c36..fec490322 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -5,19 +5,6 @@ From iris.heap_lang Require Import adequacy.
 From iris.program_logic Require Import ownership.
 From iris.heap_lang Require Import proofmode notation.
 
-(* FIXME or remove
-Section LangTests.
-  Definition add : expr := #21 + #21.
-  Goal ∀ σ, head_step add σ (#42) σ [].
-  Proof. intros; do_head_step done. Qed.
-  Definition rec_app : expr := (rec: "f" "x" := "f" "x") #0.
-  Goal ∀ σ, head_step rec_app σ rec_app σ [].
-  Proof. intros. rewrite /rec_app. do_head_step done. Qed.
-  Definition lam : expr := λ: "x", "x" + #21.
-  Goal ∀ σ, head_step (lam #21)%E σ add σ [].
-  Proof. intros. rewrite /lam. do_head_step done. Qed.
-End LangTests. *)
-
 Section LiftingTests.
   Context `{heapG Σ}.
   Implicit Types P Q : iProp Σ.
-- 
GitLab