diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 262779c360d0b5f99887c38443cad8b22aabbf6a..fec4903222f412abc0f6832a478be7ac4ae56b8f 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 Σ.