Skip to content
Snippets Groups Projects
Commit bd0e6352 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add tactic `set_unfold in H`.

parent ddd73df1
No related branches found
No related tags found
No related merge requests found
......@@ -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)
......
......@@ -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) :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment