From c95907b9b12b7b5f9b5c6d2e8b72219283ff6533 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Sep 2017 22:29:26 +0200
Subject: [PATCH] Simplify solve_to_val.
---
theories/heap_lang/tactics.v | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 97a7b0a7a..37af82a7d 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -210,6 +210,7 @@ Ltac solve_closed :=
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_to_val :=
+ rewrite /IntoVal;
try match goal with
| |- context E [language.to_val ?e] =>
let X := context E [to_val e] in change X
@@ -218,9 +219,6 @@ Ltac solve_to_val :=
| |- 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; unfold W.to_expr; reflexivity
- | |- IntoVal ?e ?v =>
- let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
- 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
--
GitLab