diff --git a/theories/hlist.v b/theories/hlist.v
index a13681e0df0387ccb070d193376b844d236adb73..6f4c5227b7b1d9468d3791bbcd9e965fd9825ce5 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -1,4 +1,5 @@
 From stdpp 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.