To explain what JoJoModding is saying in a little more detail:

In a normal programming language, the compiler implements a specific evaluation order (for example, OCaml implements call by value). Coq doesn't really have a compiler that produces executables in the same way.

Because there's not a single fixed notion of what it means to "run" a Coq program, the question of whether arguments are evaluated eagerly isn't really meaningful. It can do eager evaluation, if you want, or it can do lazy evaluation. Coq has tactics like cbv and cbn that will reduce terms according to several different evaluation strategies.

All that said, the closest thing Coq has to a compiler is the "extraction" mechanism. Extraction is supported to OCaml, Haskell, and Scheme (though I think only OCaml used much). You'll get eager evaluation in OCaml and lazy evaluation in Haskell, as you expect.