aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r--theories/Numbers/NatInt/NZDomain.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 7afbee4a42..05508c4f36 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -45,7 +45,7 @@ Qed.
Global Instance iter_wd (R:relation A) : Proper ((R==>R)==>eq==>R==>R) iter.
Proof.
-intros R f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
+intros f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
Qed.
End Iter.
@@ -412,4 +412,4 @@ Proof.
rewrite ofnat_succ, pred_succ; auto with arith.
Qed.
-End NZOfNatOps. \ No newline at end of file
+End NZOfNatOps.