It seems that Lombardi and Quitté in their book "Commutative Algebra: Constructive Methods" define UFDs as GCD-domains such that every regular element is a product of irreducibles. In classical logic, this coincides with the usual definition.