blob: d408557d50edf82d929f4b3739a9a713c355df54 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Set Universe Polymorphism.
Section foo.
Let U := Type.
Let U' : Type.
Proof.
let U' := constr:(Type) in
let U_le_U' := constr:(fun x : U => (x : U')) in
exact U'.
Defined.
Inductive t : U' := .
End foo.
(* Toplevel input, characters 15-23:
Error: No such section variable or assumption: U'. *)
|
