It's more a question of if there are any other known inconsistencies in Coq that could be used to trivially generate proofs which are artificial under human scrutiny but OK by an automated proof market.
You'd run into a problem if you let workers introduce assumptions (since introducing a contradiction lets the worker prove anything).
With Coq, you don't have a problem of unsoundness. The problem you have is that the difficulty / time it takes to write a proof is often very sensitive to how you've written your assumptions and formulated the claim. You'd likely want to add a mechanism to the marketplace to reward workers for suggesting ways to improve the problem formulation.
For my Java project, we were using ESC/Java2 under the hood which is unsound in a lot of ways. We definitely observed workers taking advantage of these (either intentionally or not).