From ae3c8fdfdd6915a543a2ff435690ec99065e2bea Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 28 Jul 2016 21:02:11 +0200
Subject: [PATCH] Make hlist universe polymorphic.

This change makes it possible to use hlists in the proof mode, which
itself uses hlists in the implementation of the specialize tactic.
---
 prelude/hlist.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/prelude/hlist.v b/prelude/hlist.v
index 8c888c732..386cc4206 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.
-- 
GitLab