aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc/non-marshalable-state/theories/evil.v
blob: 661482a9758336d11d514c687f5bc52be7eb025d (plain)
1
2
3
4
5
Declare ML Module "evil_plugin".

magic.

Lemma x : True. Proof. trivial. Qed.