From acb221ebf89253d79459274416d42053fe5b83ff Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Apr 2021 22:15:09 +0200
Subject: [PATCH] Generalize lemma `option_guard_False`.

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

diff --git a/theories/option.v b/theories/option.v
index f9b9e6ee..6a458aa4 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -345,8 +345,8 @@ Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A
     (HP : P) :
   mguard P f = f HP.
 Proof. intros. case_option_guard; [|done]. f_equal; apply proof_irrel. Qed.
-Lemma option_guard_False {A} P `{Decision P} (mx : option A) :
-  ¬P → (guard P; mx) = None.
+Lemma option_guard_False {A} P `{Decision P} (f : P → option A) :
+  ¬P → mguard P f = None.
 Proof. intros. by case_option_guard. Qed.
 Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
   (P ↔ Q) → (guard P; mx) = guard Q; mx.
-- 
GitLab