From c33ba30ec4e8ed636906d824c300788e10df20b5 Mon Sep 17 00:00:00 2001
From: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
Date: Wed, 23 Apr 2014 13:42:25 +0200
Subject: Eta contractions to please cbn

---
 theories/FSets/FMapFacts.v    |  4 ++--
 theories/FSets/FMapWeakList.v | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'theories/FSets')

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index dc33167a6..85b7242b5 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -835,8 +835,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Definition uncurry {U V W : Type} (f : U -> V -> W) : U*V -> W :=
    fun p => f (fst p) (snd p).
 
-  Definition of_list (l : list (key*elt)) :=
-    List.fold_right (uncurry (@add _)) (empty _) l.
+  Definition of_list :=
+    List.fold_right (uncurry (@add _)) (empty elt).
 
   Definition to_list := elements.
 
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 6c1e8ca89..e3f84723f 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -600,18 +600,18 @@ Definition combine_l (m:t elt)(m':t elt') : t oee' :=
 Definition combine_r (m:t elt)(m':t elt') : t oee' :=
   mapi (fun k e' => (find k m, Some e')) m'.
 
-Definition fold_right_pair (A B C:Type)(f:A->B->C->C)(l:list (A*B))(i:C) :=
-  List.fold_right (fun p => f (fst p) (snd p)) i l.
+Definition fold_right_pair (A B C:Type)(f:A->B->C->C) :=
+  List.fold_right (fun p => f (fst p) (snd p)).
 
 Definition combine (m:t elt)(m':t elt') : t oee' :=
   let l := combine_l m m' in
   let r := combine_r m m' in
-  fold_right_pair (add (elt:=oee')) l r.
+  fold_right_pair (add (elt:=oee')) r l.
 
 Lemma fold_right_pair_NoDup :
   forall l r (Hl: NoDupA (eqk (elt:=oee')) l)
     (Hl: NoDupA (eqk (elt:=oee')) r),
-    NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) l r).
+    NoDupA (eqk (elt:=oee')) (fold_right_pair (add (elt:=oee')) r l).
 Proof.
  induction l; simpl; auto.
  destruct a; simpl; auto.
@@ -733,7 +733,7 @@ Definition option_cons (A:Type)(k:key)(o:option A)(l:list (key*A)) :=
 Definition map2 m m' :=
   let m0 : t oee' := combine m m' in
   let m1 : t (option elt'') := map (fun p => f (fst p) (snd p)) m0 in
-  fold_right_pair (option_cons (A:=elt'')) m1 nil.
+  fold_right_pair (option_cons (A:=elt'')) nil m1.
 
 Lemma map2_NoDup :
   forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'),
-- 
cgit v1.2.3