blob: 12c958be67fa0394dc6908ee2b777c33072c7393 (
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. *)
|
