Skip to content

Pick universes for [bi_tforall] and [bi_texist].

Gregory Malecha requested to merge gmalecha/iris:fixpoint-tele_arg into master

Companion to stdpp!368 (merged).

This MR:

  1. updates the code to use the fixpoint versions of tele_arg
  2. Uses some explicit universe annotations to reduce the overall number of universes (very slightly). These universes are given explicit names and documented.

I think 2 is an overall improvement, but I do not think it is strictly necessary.

Merge request reports