From 1e9a5ae9400ad4ce79ee8b55bba8b3a9c71e7ace Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.org>
Date: Wed, 26 Feb 2020 21:54:56 +0100
Subject: [PATCH] Have destruct_and take care of [True] and destruct_or of
[False]
The opposite was true before to this commit.
---
theories/tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index 4fa8bb94..5b565c62 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -112,7 +112,7 @@ Tactic Notation "split_and" "!" := hnf; split_and; split_and?.
Ltac destruct_and_go H :=
try lazymatch type of H with
- | False => destruct H
+ | True => clear H
| _ ∧ _ =>
let H1 := fresh in
let H2 := fresh in
@@ -148,7 +148,7 @@ Tactic Notation "destruct_and" "!" :=
*)
Tactic Notation "destruct_or" "?" ident(H) :=
repeat match type of H with
- | True => clear H
+ | False => destruct H
| _ ∨ _ => destruct H as [H|H]
| Is_true (bool_decide _) => apply (bool_decide_unpack _) in H
| Is_true (_ || _) => apply orb_True in H; destruct H as [H|H]
--
GitLab