From 15d4aa06aad18f89b5258be56d817facb6275e7b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Mon, 29 Jul 2024 14:05:48 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#19228. (#1934) --- 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