test-suite/misc/side-eff-leak-univs/theories/evil.v


1
2
3
4
5
6
7
8
9
10

Declare ML Module "evil_plugin".

Universes i j.

Lemma foo@{} : Type@{j}.
Proof.
  magic i j; transparent_abstract exact_no_check Type@{i}.
Defined.

Definition bar : Type@{i} := Type@{j}.