blob: 83f1677455f82f88e327cbf56711661b378db43d (
plain)
1
2
3
4
5
6
7
8
9
10
|
Section foo.
Context (F : Type -> Type).
Context (admit : forall {T}, F T = True).
Hint Rewrite (fun T => @admit T).
Lemma bad : F False.
Proof.
autorewrite with core.
constructor.
Qed.
End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
|
