--- a/src/GeneralRec.v	Sun Apr 21 16:09:55 2019 -0400
+++ b/src/GeneralRec.v	Sun Feb 02 10:46:14 2020 -0500
@@ -781,6 +781,8 @@
 
 I know no easy fix for this problem of [thunk], but we can define an alternate co-inductive monad that avoids the problem, based on a proposal by Megacz%~\cite{Megacz}%.  We ran into trouble because [TBind] was not a constructor of [thunk], so let us define a new type family where "bind" is a constructor. *)
 
+Set Universe Polymorphism.
+
 CoInductive comp (A : Type) : Type :=
 | Ret : A -> comp A
 | Bnd : forall B, comp B -> (B -> comp A) -> comp A.