diff options
| author | Gaëtan Gilbert | 2018-11-09 16:23:57 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-23 13:53:17 +0100 |
| commit | 828d9447073b06a85421857d7f8b872af6cdfe6b (patch) | |
| tree | aad9cc41020a81b60bd6d5514182c06636a89357 /dev/ci/ci-iris-lambda-rust.sh | |
| parent | 90ffb19ccde90310b58e1f94eacdeed12041d86d (diff) | |
Fix printing of private universes.
Set Printing Universes.
Set Universe Polymorphism.
Lemma foo : Type.
Proof. exact (forall _ : Type, Type).
Qed.
Print foo.
Before:
(*
foo@{Top.1} =
Type@{Top.2} -> Type@{Top.3}
: Type@{Top.1}
(* Top.1 |= Prop < Set
Set < Top.1
local: {Top.3 Top.2} |= Top.2 < Top.1
Top.3 < Top.1
*)
foo is universe polymorphic
*)
Now:
(* Public universes:
Top.1 |= Set < Top.1
Private universes:
{Top.3 Top.2} |= Top.2 < Top.1
Top.3 < Top.1 *)
Diffstat (limited to 'dev/ci/ci-iris-lambda-rust.sh')
0 files changed, 0 insertions, 0 deletions