From 2f670dce285c04c66729022b2b8b8ea65bba744b Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 12 Sep 2020 18:04:01 -0700
Subject: Modify setoid_ring/Ring_theory.v to compile with -mangle-names

---
 theories/setoid_ring/Ring_theory.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/setoid_ring/Ring_theory.v b/theories/setoid_ring/Ring_theory.v
index 230e789e21..32f21e2737 100644
--- a/theories/setoid_ring/Ring_theory.v
+++ b/theories/setoid_ring/Ring_theory.v
@@ -53,7 +53,7 @@ Section Power.
 
  Lemma pow_pos_swap x j : pow_pos x j * x == x * pow_pos x j.
  Proof.
-  induction j; simpl; rewrite <- ?mul_assoc.
+  induction j as [j IHj|j IHj|]; simpl; rewrite <- ?mul_assoc.
   - f_equiv. now do 2 (rewrite IHj, mul_assoc).
   - now do 2 (rewrite IHj, mul_assoc).
   - reflexivity.
@@ -62,7 +62,7 @@ Section Power.
  Lemma pow_pos_succ x j :
    pow_pos x (Pos.succ j) == x * pow_pos x j.
  Proof.
-  induction j; simpl; try reflexivity.
+  induction j as [j IHj|j IHj|]; simpl; try reflexivity.
   rewrite IHj, <- mul_assoc; f_equiv.
   now rewrite mul_assoc, pow_pos_swap, mul_assoc.
  Qed.
@@ -70,7 +70,7 @@ Section Power.
  Lemma pow_pos_add x i j :
    pow_pos x (i + j) == pow_pos x i * pow_pos x j.
  Proof.
-  induction i using Pos.peano_ind.
+  induction i as [|i IHi] using Pos.peano_ind.
   - now rewrite Pos.add_1_l, pow_pos_succ.
   - now rewrite Pos.add_succ_l, !pow_pos_succ, IHi, mul_assoc.
  Qed.
-- 
cgit v1.2.3