From 723ad25fd59da0fa21b923929042cb5a9483c237 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Dec 2021 13:46:07 +0100
Subject: [PATCH] Add test for `destruct select`.

---
 tests/tactics.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/tests/tactics.v b/tests/tactics.v
index 659f559b..65b56cfd 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -55,6 +55,17 @@ Proof. intros ?. rename select nat into m. exists m. done. Qed.
 Goal ∀ (P : nat → Prop), P 3 → P 4 → P 4.
 Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
 
+Goal ∀ P Q : Prop, True ∨ True → P ∨ Q → Q ∨ P.
+Proof.
+  intros P Q ??. (* should select the last hypothesis *)
+  destruct select (_ ∨ _); by constructor.
+Restart.
+  intros P Q ??. (* should select the last hypothesis *)
+  destruct select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Qed.
+
 (** Regression tests for [naive_solver]. *)
 Lemma naive_solver_issue_115 (P : nat → Prop) (x : nat) :
   (∀ x', P x' → x' = 10) → P x → x + 1 = 11.
-- 
GitLab