Adapt w.r.t. coq/coq#19228. (#1934)

mit-plv · Jul 29, 2024 · 15d4aa0 · 15d4aa0
1 parent 1283287
commit 15d4aa0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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