From 4420aa4d0c7454b4824a12476e8ba0976adcd96f 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.
---
 theories/hlist.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/hlist.v b/theories/hlist.v
index a13681e0..6f4c5227 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.
-- 
GitLab