From 9ce24ee95b91000c5c1cf636b40ff772fcfc27da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sat, 27 Jul 2024 16:44:19 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#19228. (#1933) --- 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 58fa213761..1f8003f202 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -222,7 +222,7 @@ Proof. rewrite <- (option_leq_to_eq_to_leq p), <- (option_leq_to_eq_to_leq q); simpl; reflexivity. 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