From c88f1674486da846a55c0ed413cc3daf74d6f54c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Nov 2018 10:18:59 +0100
Subject: [PATCH] Heap_lang proofmode tactics: use `wp_expr_simpl` everywhere.
---
theories/heap_lang/proofmode.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 90e561f2f..eb9ef069b 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -483,7 +483,7 @@ Tactic Notation "wp_cas_fail" :=
|solve_mapsto ()
|try congruence
|try (fast_done || (left; fast_done) || (right; fast_done)) (* vals_cas_compare_safe *)
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_fail _ _ _ _ K))
@@ -510,7 +510,7 @@ Tactic Notation "wp_cas_suc" :=
|pm_reflexivity
|try congruence
|try fast_done (* vals_cas_compare_safe *)
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
--
GitLab