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

JasonGross · Jul 27, 2024 · 5a9a1b7 · 5a9a1b7
1 parent dc100dd
commit 5a9a1b7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Util/Option.v b/theories/Util/Option.v
@@ -305,7 +305,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)
+Definition invert_Some {A : Type} (x : option A)
   : (if x then A else unit)
   := match x with
      | Some x' => x'