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

Add tactics `destruct select`.

parent d9e55d3d
No related branches found
No related tags found
1 merge request!352Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 0 deletions
theories/tactics.v
+ 5
− 0
View file @ a1272450
...@@ -599,6 +599,11 @@ Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => rever ...@@ -599,6 +599,11 @@ Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => rever
Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) := Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
select pat (fun H => rename H into name). select pat (fun H => rename H into name).
Tactic Notation "destruct" "select" open_constr(pat) :=
select pat (fun H => destruct H).
Tactic Notation "destruct" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
select pat (fun H => destruct H as ipat).
(** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise. (** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
By closed we mean that [t] does not depend on any variable bound in the context. By closed we mean that [t] does not depend on any variable bound in the context.
axioms are considered closed terms by this tactic (but Section axioms are considered closed terms by this tactic (but Section
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment