3 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index ba592507b1..a5ef02570b 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -110,7 +110,7 @@ Implicit Arguments recursion [A].
 Instance recursion_wd A (Aeq : relation A) :
  Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A).
 Proof.
-intros A Aeq a a' Eaa' f f' Eff'.
+intros a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nrect.
 intros x' H; now rewrite <- H.
 clear x.
@@ -200,4 +200,4 @@ end.
 Time Eval vm_compute in (binlog 500000). (* 0 sec *)
 Time Eval vm_compute in (binlog 1000000000000000000000000000000). (* 0 sec *)
 
-*)
-\ No newline at end of file
+*)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 491c33666c..5e3ecd6885 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -126,7 +126,7 @@ Implicit Arguments recursion [A].
 Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
-intros A Aeq a a' Ha f f' Hf n n' Hn. subst n'.
+intros a a' Ha f f' Hf n n' Hn. subst n'.
 induction n; simpl; auto. apply Hf; auto.
 Qed.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 8cbd96c1fb..f4641446bb 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -200,7 +200,7 @@ Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
 unfold eq.
-intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
+intros a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
 unfold N.to_N.
 rewrite <- Exx'; clear x' Exx'.