v8.4: Backporting Matthieu's trunk commit r16134 (eta was missing in
Flexible/Rigid and SemiFlexible/Rigid conversion problems). This
commit solved bug #3023. Also added regression test for this bug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16410 85f007b7-540e-0410-9357-904b9bb8a0f7