From 6d64bcb55e53563f6ec4ea84aa0ba5a8a1c55aa0 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Mon, 16 May 2022 14:14:30 +0200
Subject: [PATCH] Enable cumulativity for telescopes.
---
tests/telescopes.v | 9 +++++++++
theories/telescopes.v | 1 +
2 files changed, 10 insertions(+)
diff --git a/tests/telescopes.v b/tests/telescopes.v
index d231e291..416d29c8 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -79,3 +79,12 @@ Example tele_arg_notation_2_dep : [tele (b : bool) (_ : if b then nat else False
assert_succeeds exact [tele_arg true; 0].
assert_succeeds refine [tele_arg true; 0].
Abort.
+
+(* Assert that telescopes are cumulatively universe polymorphic.
+ See https://gitlab.mpi-sws.org/iris/iris/-/issues/461
+ *)
+Section Cumulativity.
+ Monomorphic Universes Quant local.
+ Monomorphic Constraint local < Quant.
+ Example cumul (t : tele@{local}) : tele@{Quant} := t.
+End Cumulativity.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 2378216e..33f44ad9 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -2,6 +2,7 @@ From stdpp Require Import base tactics.
From stdpp Require Import options.
Local Set Universe Polymorphism.
+Local Set Polymorphic Inductive Cumulativity.
(** Without this flag, Coq minimizes some universes to [Set] when they
should not be, e.g. in [texist_exist].
--
GitLab