diff options
| author | letouzey | 2010-09-17 14:12:55 +0000 |
|---|---|---|
| committer | letouzey | 2010-09-17 14:12:55 +0000 |
| commit | 2a35022f6e0ed8b5a2b2fce5077104cfa6cea1b3 (patch) | |
| tree | a8ed6f19565ba1c7cc962dba5df50f9f581e1fbd | |
| parent | 0931ccb78d2555e5c38da66a2e2cd7afc6ae7e94 (diff) | |
For the moment, two small manual eta-expansions to avoid '_a after extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13425 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index f9dda51255..684291d7ce 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 := elements_aux nil. +Definition elements m := elements_aux nil m. (** * Fold *) diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index 349cdedf7b..fee3f5bcfc 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -328,7 +328,7 @@ Fixpoint elements_aux (acc : list X.t) (s : t) : list X.t := (** then [elements] is an instanciation with an empty [acc] *) -Definition elements := elements_aux nil. +Definition elements s := elements_aux nil s. (** ** Filter *) |