blob: 6ca36da4b062c9ad05dc9be44bcc0de34dbbbfa1 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* -*- coq-prog-args: ("-async-proofs" "on"); -*- *)
Unset Universe Polymorphism.
Ltac exact0 := let x := constr:(Type) in exact 0.
Lemma lemma_restrict_abstract@{} : (nat * nat)%type.
Proof. split;[exact 0|abstract exact0]. Qed.
(* Debug: 10237:proofworker:0:0 STM: sending back a fat state
Error: Universe {polymorphism.1} is unbound. *)
|
