Unset Universe Minimization ToSet in monad_utils

MetaCoq · Apr 20, 2023 · 24241a5 · 24241a5
1 parent 088871f
commit 24241a5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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