- Fix evarconv so that we have complete eta-conversion:
  - In the maybeflex/rigid (lambda) case, try eta if the maybeflex doesn't
actually unfold (e.g. vars, or the transparent state says it's opaque).
  - In the flexible/rigid(lambda) case, try eta if miller-pfenning fails
(as the stack might not be a purely applicative one). This will zip the
flexible term (a case construct most likely) and try eta expansion on it.


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