Modify ZArith/Zpower.v to compile with -mangle-names

1 files changed, 5 insertions, 5 deletions

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 6f464d89bb..6b01d798e4 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp :
   forall (n m:nat) (z:Z),
     Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
 Proof.
- induction n.
+ intros n; induction n as [|n IHn].
  - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
  - intros. simpl. now rewrite IHn, Z.mul_assoc.
 Qed.
@@ -135,7 +135,7 @@ Section Powers_of_2.
 
   Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).
   Proof.
-   induction n.
+   induction n as [|n IHn].
    - trivial.
    - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg.
   Qed.
@@ -164,7 +164,7 @@ Section Powers_of_2.
   Theorem shift_nat_correct n x :
     Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
   Proof.
-   induction n.
+   induction n as [|n IHn].
    - trivial.
    - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn.
   Qed.
@@ -295,7 +295,7 @@ Section power_div_with_rest.
      rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc.
      repeat split; auto.
      rewrite !Z.mul_1_l, H, Z.add_assoc.
-     apply f_equal2 with (f := Z.add); auto.
+     apply (f_equal2 Z.add); auto.
      rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r.
      now rewrite Z.mul_1_l.
    - rewrite Pos2Z.neg_xO in H.
@@ -303,7 +303,7 @@ Section power_div_with_rest.
      repeat split; auto.
    - repeat split; auto.
      rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc.
-     apply f_equal2 with (f := Z.add); auto.
+     apply (f_equal2 Z.add); auto.
      rewrite Z.add_comm, <- Z.add_diag.
      rewrite Z.mul_add_distr_l.
      replace (-1 * d) with (-d).