Fixing #3089. This implied tweaking the definition of the lexicographic
product of lists, hence possibly introducing incompatibilities.

Parts of the patch by Chantal Keller.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7