From 98f73a0b425c53b38fe193ee7460bdbf5754a2a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Jan 2017 19:27:20 +0100
Subject: [PATCH] Perform a simpl after wp_apply.

wp_apply often results in an of_val that should be simplified.
---
 theories/heap_lang/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 007242549..a793ec715 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -222,7 +222,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
   iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    wp_bind_core K; iApply lem; try iNext)
+    wp_bind_core K; iApply lem; try iNext; simpl)
   | _ => fail "wp_apply: not a 'wp'"
   end.
 
-- 
GitLab