Often times proofs in ZF which do not use the axiom of choice are called constructive, but of course really it is easy to create non constructive proofs using LEM. Is there a precise sense in which ZF is more constructive than working without LEM in the logic?
Basically I am asking what is the advantage of proving things in ZF vs. ZFC when ZF is also not constructive. Is there a certain notion which says that if I prove something in ZF then there is a way in which my proof is a little more constructive? How to make the notion of little more precise.