From 5ad12cd3e5847fe8d43538a37fc5fed771d0270b Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 3 May 2021 12:50:46 +0200 Subject: [PATCH] Also write `option_guard_True` using `mguard` (instead of `guard` notation). --- theories/option.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/option.v b/theories/option.v index 6a458aa4..7c10bc43 100644 --- a/theories/option.v +++ b/theories/option.v @@ -339,7 +339,7 @@ Tactic Notation "case_option_guard" := let H := fresh in case_option_guard as H. Lemma option_guard_True {A} P `{Decision P} (mx : option A) : - P → (guard P; mx) = mx. + P → mguard P (λ _, mx) = mx. Proof. intros. by case_option_guard. Qed. Lemma option_guard_True_pi {A} P `{Decision P, ProofIrrel P} (f : P → option A) (HP : P) : -- GitLab