Commit 6d64bcb5 authored by Jan-Oliver Kaiser's avatar Jan-Oliver Kaiser
Browse files

Enable cumulativity for telescopes.

parent 8b17ca72
......@@ -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.
......@@ -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].
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment