From 60645f9bbd9e75940028ca469558cbadca73f3d2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Apr 2021 22:16:08 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`decide=5Fleft`=20=E2=86=92=20`decide?=
 =?UTF-8?q?=5FTrue=5Fpi`,=20`decide=5Fright`=20=E2=86=92=20`decide=5FFalse?=
 =?UTF-8?q?=5Fpi`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/decidable.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index 310eff9a..89b74b2e 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -25,9 +25,9 @@ Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
   (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
 Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
 
-Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
+Lemma decide_True_pi `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
 Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed.
-Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
+Lemma decide_False_pi `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
 Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed.
 
 (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
-- 
GitLab