diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v
index 5e38af191a..3f8d22aee3 100644
--- a/utils/theories/monad_utils.v
+++ b/utils/theories/monad_utils.v
@@ -6,6 +6,7 @@ Coercion is_true : bool >-> Sortclass.
 Import ListNotations.
 
 Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
 
 Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
 { ret : forall {t : Type@{d}}, t -> m t