It seems that Lombardi and Quitté in their book "[Commutative Algebra: Constructive Methods][1]", Ch. XI, §3, define UFDs as GCD-domains such that every regular element is a product of irreducibles. In classical logic, this coincides with the usual definition. (Ingo sketched the proof in his comment.)


  [1]: http://hlombardi.free.fr/CACM.pdf