From 2a35022f6e0ed8b5a2b2fce5077104cfa6cea1b3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 17 Sep 2010 14:12:55 +0000
Subject: 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
---
 theories/FSets/FMapAVL.v | 2 +-
 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 *)
 
-- 
cgit v1.2.3