From efd82c63aef1542d48139f5dca685b625ac23058 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Feb 2016 20:52:12 +0100
Subject: [PATCH] Remove FIXME, it is due to a Set Printing all above.

---
 heap_lang/tests.v | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 8c0058204..dbfd09cb0 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -9,14 +9,10 @@ Module LangTests.
   Proof. intros; do_step done. Qed.
   Definition rec_app : expr := (rec:: #0 #1) (Lit 0).
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
-  Proof. Set Printing All. intros; do_step done. Qed.
+  Proof. intros; do_step done. Qed.
   Definition lam : expr := λ: #0 + Lit 21.
   Goal ∀ σ, prim_step (lam (Lit 21)) σ add σ None.
-  Proof.
-    (* FIXME WTF why does it print all the "S (S (S..."?? *)
-    rewrite /lam /Lam.
-    intros; do_step done.
-  Qed.
+  Proof. rewrite /lam /Lam. intros; do_step done. Qed.
 End LangTests.
 
 Module LiftingTests.
-- 
GitLab