blob: fe9772dc628edc97e106d8cbfb44e882496c4d9b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Polymorphic Axiom foo@{u} : Prop -> Prop.
Arguments foo {_}.
Axiom bla : forall {A B}, @foo A -> @foo B -> Prop.
Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y.
Print thing. (* forall x y : foo, bla x y *)
Set Printing Universes.
Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *)
Set Printing Implicit.
Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *)
|
