Library Mtac2Tests.test_ret
Require
Import
Mtac2.Mtac2
.
Goal
True
.
MProof
.
M.ret
I
.
Qed
.