Formal semantics of OCaml in Coq The semantics of a large subset of OCaml, called OCamllight,  was formalized in HOL by Owens several years ago. More recently, a type theoretical semantics of a smaller subset of OCaml was implemented in Nuprl by Kreitz, Hayden and Hickey. 

Is there any similar development in Coq?
Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? 

Rather than building the type system and small-step semantics as inductive relations, he gives a technique for converting Caml programs into characteristic formulas. This are basically a generalization of predicate transformer semantics to support a very large subset of Ocaml -- notably, including unsafe casts like Obj.magic. To quote from his thesis:


  I have focused on a subset of the OCaml programming lan-
  guage, which is a sequential, call-by-value, high-level programming language. The
  current implementation of CFML supports the core λ-calculus, including higher-
  order functions, recursion, mutual recursion and polymorphic recursion. It supports
  tuples, data constructors, pattern matching, reference cells, records and arrays. I
  provide an additional Caml library that adds support for null pointers and strong
  updates.


It's a very appealing approach if you want to prove a particular Caml program correct (less so if you are interested in its metatheory, though).