Cosmetic on printing + rewriting of some test functions to make them terminate in Coq