diff options
| author | Jasper Hugunin | 2020-09-12 18:04:01 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 2f670dce285c04c66729022b2b8b8ea65bba744b (patch) | |
| tree | d459cc201d67931b5e5102cb50b219ce5bccc120 | |
| parent | 9daa2ec464eb9b881cab7d53fd39efc5de3afe12 (diff) | |
Modify setoid_ring/Ring_theory.v to compile with -mangle-names
| -rw-r--r-- | theories/setoid_ring/Ring_theory.v | 6 |
1 files 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. |