blob: 7fd98c2773cffb2c080a654f21677f04e826b527 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Declare ML Module "evil_plugin".
Evil T f. (* <- if this doesn't fail then the rest goes through *)
Definition g : Type -> Set := f.
Require Import Hurkens.
Lemma absurd : False.
Proof.
exact (TypeNeqSmallType.paradox (g Type) eq_refl).
Qed.
|
