This project aims at providing a framework for program transformation by equational reasoning where each step are verified in Coq.
This project aims at improving the coq-tex tool.