Coinduction 1.2, for Coq 8.13
Fixed handling of universes in OCaml plugin,
new helpers for proving that contextual functions are below the companion.
Fixed handling of universes in OCaml plugin,
new helpers for proving that contextual functions are below the companion.