Make Monad a cumulative inductive type

JasonGross · Apr 2, 2023 · 2442088 · 2442088
1 parent 1a43883
commit 2442088
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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