From 42a8dc3abea9bdae18315595bc7108f5c229f8c1 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Wed, 28 Feb 2018 17:47:52 +0100
Subject: [PATCH] Try `<:` (VMcast) for instances of `exact I`.
---
theories/lang/tactics.v | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index a7d8e6e5..f628f502 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -172,7 +172,8 @@ Ltac solve_closed :=
match goal with
| |- Closed ?X ?e =>
let e' := W.of_expr e in change (Closed X (W.to_expr e'));
- apply W.is_closed_correct; vm_compute; exact I
+ (* apply W.is_closed_correct; vm_compute; exact I *)
+ apply W.is_closed_correct; exact (I <: W.is_closed X e')
end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
@@ -188,7 +189,11 @@ Ltac solve_to_val :=
apply W.to_val_Some; simpl; unfold W.to_expr; unlock; 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
+ apply W.to_val_is_Some, (bool_decide_unpack _);
+ (* vm_compute; exact I *)
+ match goal with [|-Is_true (@bool_decide ?P ?dec)] =>
+ exact (I <: Is_true (@bool_decide P dec))
+ end
end.
Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
@@ -197,7 +202,8 @@ Ltac solve_atomic :=
match goal with
| |- Atomic ?s ?e =>
let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
- apply W.is_atomic_correct; vm_compute; exact I
+ (* apply W.is_atomic_correct; vm_compute; exact I *)
+ apply W.is_atomic_correct; exact (I <: W.is_atomic e')
end.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
--
GitLab