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