We present ongoing work on verified compilation of imperative functional code in Coq, relying on the CompCert C compiler and using a reflective approach. Here we focus on the reflection of a monadic fragment of Gallina, corresponding to a first-order imperative language with primitive recursion, in a deeply embedded extensible language that we call DEC2 and which can be translated to the CompCert C front-end. DEC2 has an operational interpreter based on small-step semantics, and a denotational interpreter based on its reflective translation into Gallina. In particular, here we will focus on the technique used in proving the adequacy of reflection, by constructing the two interpreters together with a proof of their extensional equality.