Extraction: re-introduce some eta-expansions in rare situations leading to '_a types

 If there's no lambdas at the top of a constant body
  and its type is functional
  and this type contains type variable
  and we're extracting to Ocaml
  then we perform one eta-expansion to please the ML type-checker

 This might slow down things, if some computations are shared
 thanks to the partial application. But it seems quite unlikely to
 encounter both situations (clever partial application and
 non-generalizable variable) at the same time. Compcert is ok,
 for instance.

 As a consequence, no need for manual eta-expansion in AVL code
 (and by the way MSetAVL.element wasn't a problem, it is monomorphic)

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

0 files changed, 0 insertions, 0 deletions