Formal semantics of OCaml 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).