Here are some interesting projects that use Coq proofs, I'll leave it up to you to judge how real world they are.

Generate OCaml code from Coq: https://github.com/msgpack/msgpack-ocaml/tree/master/proof

Proof algorithms written in OCaml using Coq: http://www.chargueraud.org/softs/cfml/

Write program specification and use multiple provers (including Coq): http://why3.lri.fr/

Write certified programs, and verify proofs using Coq: http://focalize.inria.fr/

Language semantics / type system proofs of languages: http://www.cl.cam.ac.uk/~so294/ocaml/ (for a subset of OCaml)

http://gallium.inria.fr/~protzenk/mezzo-lang/

Books on Coq: http://adam.chlipala.net/cpdt/ http://www.cis.upenn.edu/~bcpierce/sf/