Proving the correctness of a type checker for a full-fledged programming language is a difficult task. As an alternative approach, we consider translating the result of type checking to Coq. The expressiveness of Gallina’s type system allows a type preserving translation, and its strong soundness properties ensures the safety of typed terms. We developed a new backend for a subset of OCaml that generates a Coq version, such that one can verify that the result of their evaluation is the intended one. We plan to extend it to cover a large part of the language.