From e46551b83d32a69ff17d7c49735869311cf6b636 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 9 Jun 2018 09:24:33 +0200
Subject: [PATCH] Fix universe inconsistency in Iris by making telescopes
 universe polymorphic

---
 theories/telescopes.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/telescopes.v b/theories/telescopes.v
index 1aaab4d1..17b70cf6 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -1,6 +1,8 @@
 From stdpp Require Import base tactics.
 Set Default Proof Using "Type".
 
+Local Set Universe Polymorphism.
+
 (** Telescopes *)
 Inductive tele : Type :=
   | TeleO : tele
-- 
GitLab