diff --git a/prelude/hlist.v b/prelude/hlist.v
index 8c888c732290a9b90917fe6d68b26ffc56ded8c1..386cc42066800d3ca7986b4521f49102dc2db8a0 100644
--- a/prelude/hlist.v
+++ b/prelude/hlist.v
@@ -1,4 +1,5 @@
 From iris.prelude Require Import tactics.
+Local Set Universe Polymorphism.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
 Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.