Merge pull request #896 from JasonGross/coq-8.16+on-some-none-poly

Make `on_some{,_or_none}` universe polymorphic
MetaCoq · Apr 5, 2023 · 61a1b43 · 61a1b43
2 parents 481ed02 + 3c755e1
commit 61a1b43
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/utils/theories/MCOption.v b/utils/theories/MCOption.v
@@ -8,7 +8,7 @@ Definition option_get {A} (default : A) (x : option A) : A
      | None => default
      end.
 
-Definition on_some {A} (P : A -> Type) (o : option A) :=
+Polymorphic Definition on_some {A} (P : A -> Type) (o : option A) :=
   match o with
   | Some t => P t
   | None => False
@@ -27,7 +27,7 @@ Proof.
 Qed.
 
 
-Definition on_some_or_none {A} (P : A -> Type) : option A -> Type :=
+Polymorphic Definition on_some_or_none {A} (P : A -> Type) : option A -> Type :=
   fun x => match x with
         | Some x => P x
         | None => True