Added a draft for coq version.
Some testing on ml style.