  We give a constructive proof that $R[X]$ is normal when $R$ is normal. We
apply this result to an operation needed for studying the henselization of a
local ring. Our proof is based on the case where $R$ is without zero divisors,
which is more involved than the case where $R$ is an integral domain. We have
to use a constructive deciphering technique that replaces the use of minimal
primes (in classical mathematics) by suitable explicit localizations in a
suitable tree.
