diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-20 14:54:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-20 14:54:01 +0000 |
| commit | 4102fedccf34dc3f759685cda7018c605be1c22c (patch) | |
| tree | e7f43604ce719ee8f5bc73d0b0d6b4223698b3ff /theories/FSets/FMapAVL.v | |
| parent | 0c4a086210c6366c9ee1f091cc51ea5c92b5a903 (diff) | |
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
Diffstat (limited to 'theories/FSets/FMapAVL.v')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 684291d7c..f9dda5125 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) := (** then [elements] is an instanciation with an empty [acc] *) -Definition elements m := elements_aux nil m. +Definition elements := elements_aux nil. (** * Fold *) |