From b513b2b6da456164f8551d9ac4cc9305b4e4dc8c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 28 Jul 2024 22:54:52 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#19228. --- src/Util/Option.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/Option.v b/src/Util/Option.v index 7e0707d1ba..78a964e7b4 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -323,7 +323,7 @@ Definition is_Some {A} (x : option A) : bool Lemma is_None_eq_None_iff {A x} : @is_None A x = true <-> x = None. Proof. destruct x; cbv; split; congruence. Qed. -Definition invert_Some {A} (x : option A) : match x with +Definition invert_Some {A : Type} (x : option A) : match x with | Some _ => A | None => unit end