diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v index 0944c1a54..77f04e1c2 100644 --- a/utils/theories/monad_utils.v +++ b/utils/theories/monad_utils.v @@ -7,6 +7,7 @@ Import ListNotations. Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. +Unset Universe Minimization ToSet. Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type := { ret : forall {t : Type@{d}}, t -> m t