From 4e2b08600b68c6d4d1197b5ff03b9248b3034ffc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jul 2016 21:29:17 +0200
Subject: [PATCH] Some tweaks.
---
heap_lang/tactics.v | 4 ++--
tests/list_reverse.v | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index f2206fed0..6ac1972a7 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -206,7 +206,7 @@ Ltac solve_to_val :=
match goal with
| |- to_val ?e = Some ?v =>
let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
- apply W.to_val_Some; simpl; reflexivity
+ apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
| |- is_Some (to_val ?e) =>
let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
@@ -227,7 +227,7 @@ Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
(** Substitution *)
Ltac simpl_subst :=
- csimpl;
+ simpl;
repeat match goal with
| |- context [subst ?x ?er ?e] =>
let er' := W.of_expr er in let e' := W.of_expr e in
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 647aa6749..680c02a6f 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -32,7 +32,7 @@ Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp) :
⊢ WP rev hd acc {{ Φ }}.
Proof.
iIntros "(#Hh & Hxs & Hys & HΦ)".
- iLöb (hd acc xs ys Φ) as "IH". wp_rec; wp_let.
+ iLöb (hd acc xs ys Φ) as "IH". wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
--
GitLab