blob: 399947f00f032890a9bd2923dfcccf20e6e6508b (
plain)
1
2
3
4
5
6
7
8
|
Require Import Coq.Program.Tactics.
Set Universe Polymorphism.
Set Printing Universes.
Definition typ := Type.
Program Definition foo : typ := _ -> _.
Next Obligation. Admitted.
Next Obligation. exact typ. Show Proof. Show Universes. Defined.
|
