From bd0e63529050c2a449af9ab1b7fec14502588432 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Mar 2020 15:29:16 +0100
Subject: [PATCH] Add tactic `set_unfold in H`.
---
CHANGELOG.md | 1 +
theories/sets.v | 9 ++++++++-
2 files changed, 9 insertions(+), 1 deletion(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd01e92c..231ee8fb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -27,6 +27,7 @@ API-breaking change is listed.
Slight breaking change: `destruct_and` no longer handle `False`;
`destruct_or` now handles `False` while `destruct_and` handles `True`,
as the respective units of disjunction and conjunction.
+- Add tactic `set_unfold in H`.
## std++ 1.2.1 (released 2019-08-29)
diff --git a/theories/sets.v b/theories/sets.v
index c6bdf3e4..6841be61 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -304,7 +304,7 @@ Section set_unfold_list.
Qed.
End set_unfold_list.
-Ltac set_unfold :=
+Tactic Notation "set_unfold" :=
let rec unfold_hyps :=
try match goal with
| H : ?P |- _ =>
@@ -317,6 +317,13 @@ Ltac set_unfold :=
end in
apply set_unfold_2; unfold_hyps; csimpl in *.
+Tactic Notation "set_unfold" "in" ident(H) :=
+ let P := type of H in
+ lazymatch type of P with
+ | Prop => apply set_unfold_1 in H
+ | _ => fail "hypothesis" H "is not a proposition"
+ end.
+
(** Since [firstorder] already fails or loops on very small goals generated by
[set_solver], we use the [naive_solver] tactic as a substitute. *)
Tactic Notation "set_solver" "by" tactic3(tac) :=
--
GitLab