aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FMapAVL.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-17 14:12:55 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-17 14:12:55 +0000
commit2a35022f6e0ed8b5a2b2fce5077104cfa6cea1b3 (patch)
treea8ed6f19565ba1c7cc962dba5df50f9f581e1fbd /theories/FSets/FMapAVL.v
parent0931ccb78d2555e5c38da66a2e2cd7afc6ae7e94 (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
Diffstat (limited to 'theories/FSets/FMapAVL.v')
-rw-r--r--theories/FSets/FMapAVL.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f9dda5125..684291d7c 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 *)