From a1272450c1d588de2cc0229e74e16ad05569c6ba Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Dec 2021 13:43:24 +0100
Subject: [PATCH] Add tactics `destruct select`.

---
 theories/tactics.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/tactics.v b/theories/tactics.v
index 744ec4b7..2baea53c 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -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) :=
   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.
 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
-- 
GitLab