Coq is constructive be default, but you can add the axiom of choice and the law of the excluded middle to make it classical (other common axioms are functional extensionality, propositional extensionality, and proof irrelevance).

Perhaps you are recalling Godel's incompleteness theorem, which says that for any finite formal system (like Coq) there exists a true theorem it is unable to prove?