Eta contractions to please cbn

10 files changed, 28 insertions, 27 deletions

diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 018b5c83f..68add5b3d 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -141,8 +141,8 @@ Qed.
 
 Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
 Definition PolEnv := Env R. (* For interpreting PolC *)
-Definition eval_pol (env : PolEnv) (p:PolC) : R :=
-   Pphi rplus rtimes phi env p.
+Definition eval_pol : PolEnv -> PolC -> R :=
+   Pphi rplus rtimes phi.
 
 Inductive Op1 : Set := (* relations with 0 *)
 | Equal (* == 0 *)
@@ -679,7 +679,8 @@ match o with
 | OpGt => fun x y : R => y < x
 end.
 
-Definition  eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe.
+Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
+ PEeval rplus rtimes rminus ropp phi pow_phi rpow.
 
 Record Formula (T:Type) : Type := {
   Flhs : PExpr T;
@@ -910,7 +911,7 @@ Proof.
   unfold pow_N. ring.
 Qed.
 
-Definition denorm (p : Pol C)  := xdenorm xH p.
+Definition denorm := xdenorm xH.
 
 Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
 Proof.
@@ -960,8 +961,8 @@ Definition map_Formula (f : Formula S)  : Formula C :=
     Build_Formula (map_PExpr l) o (map_PExpr r).
 
 
-Definition eval_sexpr (env : PolEnv) (e : PExpr S) : R :=
-  PEeval rplus rtimes rminus ropp phiS pow_phi rpow env e.
+Definition eval_sexpr : PolEnv -> PExpr S -> R :=
+  PEeval rplus rtimes rminus ropp phiS pow_phi rpow.
 
 Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop :=
   let (lhs, op, rhs) := f in
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index d7162e620..5363c5465 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -60,13 +60,13 @@ Definition Bhigh := @Vector.tl bool.
 
 Definition Bsign := @Vector.last bool.
 
-Definition Bneg n (v : Bvector n) := Vector.map negb v.
+Definition Bneg := @Vector.map _ _ negb.
 
-Definition BVand n (v : Bvector n) := Vector.map2 andb v.
+Definition BVand := @Vector.map2 _ _ _ andb.
 
-Definition BVor n (v : Bvector n) := Vector.map2 orb v.
+Definition BVor := @Vector.map2 _ _ _ orb.
 
-Definition BVxor n (v : Bvector n) := Vector.map2 xorb v.
+Definition BVxor := @Vector.map2 _ _ _ xorb.
 
 Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
   Bcons carry n (Vector.shiftout bv).
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'),
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 7c8c5e6de..9743e358f 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -56,8 +56,8 @@ Module Ops (X: DecidableType) <: WOps X.
         if X.eq_dec x y then l else y :: remove x l
     end.
 
-  Definition fold (B : Type) (f : elt -> B -> B) (s : t) (i : B) : B :=
-    fold_left (flip f) s i.
+  Definition fold (B : Type) (f : elt -> B -> B) : t -> B -> B :=
+    fold_left (flip f).
 
   Definition union (s : t) : t -> t := fold add s.
 
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 3c0bbbad9..c4e6bd254 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -325,8 +325,8 @@ Definition lxor n m :=
 
 (** Shifts *)
 
-Definition shiftl_nat (a:N)(n:nat) := nat_rect _ a (fun _ => double) n.
-Definition shiftr_nat (a:N)(n:nat) := nat_rect _ a (fun _ => div2) n.
+Definition shiftl_nat (a:N) := nat_rect _ a (fun _ => double).
+Definition shiftr_nat (a:N) := nat_rect _ a (fun _ => div2).
 
 Definition shiftl a n :=
   match a with
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 6674943a6..4541fce0d 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -482,8 +482,8 @@ Fixpoint lxor (p q:positive) : N :=
 
 (** Shifts. NB: right shift of 1 stays at 1. *)
 
-Definition shiftl_nat (p:positive)(n:nat) := nat_rect _ p (fun _ => xO) n.
-Definition shiftr_nat (p:positive)(n:nat) := nat_rect _ p (fun _ => div2) n.
+Definition shiftl_nat (p:positive) := nat_rect _ p (fun _ => xO).
+Definition shiftr_nat (p:positive) := nat_rect _ p (fun _ => div2).
 
 Definition shiftl (p:positive)(n:N) :=
   match n with
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index cf5bb3f2a..5acdd8292 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -925,8 +925,8 @@ Qed.
 
 (** * Rational to the n-th power *)
 
-Definition Qpower_positive (q:Q)(p:positive) : Q :=
- pow_pos Qmult q p.
+Definition Qpower_positive : Q -> positive -> Q :=
+ pow_pos Qmult.
 
 Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive.
 Proof.
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index fa8f5c275..8a9497682 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -41,7 +41,7 @@ Section VALUE_OF_BOOLEAN_VECTORS.
 
   Lemma binary_value : forall n:nat, Bvector n -> Z.
   Proof.
-    simple induction n; intros.
+    refine (nat_rect _ _ _); intros.
     exact 0%Z.
 
     inversion H0.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 616445d06..7ccaa119c 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -25,7 +25,7 @@ Local Open Scope Z_scope.
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_nat (z:Z) (n:nat) := nat_rect _ 1 (fun _ => Z.mul z) n.
+Definition Zpower_nat (z:Z) := nat_rect _ 1 (fun _ => Z.mul z).
 
 Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
 Proof. reflexivity. Qed.