From 47598d44b83bba9151d3f43de74038069c44caf1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Feb 2016 23:45:41 +0100
Subject: [PATCH] Block simpl for of_val to avoid too much unfolding.

---
 heap_lang/lifting.v |  1 +
 heap_lang/tests.v   | 11 +++++------
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index c52e34a7e..068d8237d 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -8,6 +8,7 @@ Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 in case [e] does not contain the free variable [x] it will return [e] in a
 way that is syntactically equal (i.e. without any Coq-level delta reduction
 performed) *)
+Arguments of_val : simpl never.
 Definition gsubst_lift {A B C} (f : A → B → C)
     (x : A) (y : B) (mx : option A) (my : option B) : option C :=
   match mx, my with
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index c6745e3ab..a82696c7e 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -92,15 +92,14 @@ Module LiftingTests.
     rewrite -(wp_bindi (IfCtx _ _)) /=.
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_if_true.
-      rewrite -(wp_bindi (UnOpCtx _)).
-      rewrite -(wp_bind [AppLCtx _; AppRCtx FindPred]).
-      rewrite -(wp_bindi (BinOpLCtx _ _)).
+      rewrite -(wp_bindi (UnOpCtx _)) /=.
+      rewrite -(wp_bind [AppLCtx _; AppRCtx _]) /=.
+      rewrite -(wp_bindi (BinOpLCtx _ _)) /=.
       rewrite -wp_un_op //=.
       rewrite -wp_bin_op //= -!later_intro.
       rewrite -FindPred_spec. apply and_intro; first by (apply const_intro; omega).
       rewrite -wp_un_op //= -later_intro.
-      assert (n - 1 = - (- n + 2 - 1)) as EQ by omega.
-      by rewrite EQ.
+      by assert (n - 1 = - (- n + 2 - 1)) as -> by omega.
     - rewrite -wp_if_false.
       rewrite -!later_intro -FindPred_spec.
       auto using and_intro, const_intro with omega.
@@ -112,6 +111,6 @@ Module LiftingTests.
   Proof.
     intros E.
     rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
-    rewrite -Pred_spec -!later_intro /=. by apply const_intro.
+    by rewrite -Pred_spec -!later_intro /=.
   Qed.
 End LiftingTests.
-- 
GitLab