From d0d517b37ba3438f767cb8c3e395dbbabfe252fe Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 20 Apr 2023 14:15:30 -0700 Subject: [PATCH] Unset Universe Minimization ToSet in monad_utils --- utils/theories/monad_utils.v | 1 + 1 file changed, 1 insertion(+) 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