diff --git a/src/itree/ITreeLang.v b/src/itree/ITreeLang.v
index 9893582..b4dcfae 100644
--- a/src/itree/ITreeLang.v
+++ b/src/itree/ITreeLang.v
@@ -35,9 +35,9 @@ From PromisingLib Require Import Event.
 Require Export ITreeLib.
 Require Export Program.
 
+Set Universe Polymorphism.
 Set Implicit Arguments.
 
-
 Module MemE.
   Variant rmw :=
   | fetch_add (addendum:Const.t)
diff --git a/src/model/Configuration.v b/src/model/Configuration.v
index 67c9b95..f9893c8 100644
--- a/src/model/Configuration.v
+++ b/src/model/Configuration.v
@@ -20,6 +20,7 @@ Require Import Global.
 Require Import Local.
 Require Import Thread.
 
+Set Universe Polymorphism.
 Set Implicit Arguments.
 
 
diff --git a/src/trans/Compatibility.v b/src/trans/Compatibility.v
index cc4f3da..e5b8783 100644
--- a/src/trans/Compatibility.v
+++ b/src/trans/Compatibility.v
@@ -33,6 +33,7 @@ Require Import SimMemory.
 Require Import SimGlobal.
 Require Import SimThread.
 
+Set Universe Polymorphism.
 Set Implicit Arguments.