I want a Gallina implementation of an interpreter that I can extract to OCaml using Coq.

UPDATE: found it thank you.