The logic of Coq is computational: if you have a close proof of the existence of a number which satisfies some property, you can "evaluate" the proof and it'll give you the witness of the existence.
The logic of Coq does not assume excluded-middle (classical reasoning) by default. But you can postulate excluded-middle (by requiring some special file of the library, Classical.v) and Coq shall become a classical logic.
The (only) drawback is that classical logic breaks the property that a close proof of the existence of a number which satisfies some property provides the witness by evaluation. This is limitation from the computational point of view but this remains perfectly ok from the logical point of view.