blob: 9895548c1d1ce5c69ec475bd32d6388c07301f92 (
plain)
1
2
3
4
5
6
7
8
9
|
Set Printing Universes.
Definition foo : Type.
Proof.
assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat).
exact bar.
Defined. (* Toplevel input, characters 0-8:
Error:
The term "(fun _ : Set => bar) foo_subproof" has type
"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *)
|
