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.

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.
ae3c8fdf · Robbert Krebbers · 922a41c1 · ae3c8fdf
Commit ae3c8fdf authored 8 years ago by Robbert Krebbers
--- a/prelude/hlist.v
+++ b/prelude/hlist.v
 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.