diff options
| author | Pierre-Marie Pédrot | 2021-01-07 18:13:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-07 18:13:28 +0100 |
| commit | 7b946aa196490be8790cd5b46d0860b3bf6e33e1 (patch) | |
| tree | 86dd8f3ebcebda8edb2d4ae46793a310e16d062f /theories/Numbers | |
| parent | 331592e05f6f222da40489a94abdcdd3ef4b6394 (diff) | |
| parent | 46c28054eb404175e5ba9485c3b5efbfe1b81619 (diff) | |
Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... at ..." instead)
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/DecimalPos.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/HexadecimalPos.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v index 5611329b12..f86246d3c2 100644 --- a/theories/Numbers/DecimalPos.v +++ b/theories/Numbers/DecimalPos.v @@ -216,7 +216,7 @@ Proof. - trivial. - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). rewrite N.mul_succ_r. - change 10 at 2 with (Nat.iter 10%nat N.succ 0). + change 10 with (Nat.iter 10%nat N.succ 0) at 2. rewrite ?nat_iter_S, nat_iter_0. rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. destruct (to_lu (N.pos p)); simpl; auto. diff --git a/theories/Numbers/HexadecimalPos.v b/theories/Numbers/HexadecimalPos.v index 47f6d983b7..29029cb839 100644 --- a/theories/Numbers/HexadecimalPos.v +++ b/theories/Numbers/HexadecimalPos.v @@ -235,7 +235,7 @@ Proof. - trivial. - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). rewrite N.mul_succ_r. - change 0x10 at 2 with (Nat.iter 0x10%nat N.succ 0). + change 0x10 with (Nat.iter 0x10%nat N.succ 0) at 2. rewrite ?nat_iter_S, nat_iter_0. rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. destruct (to_lu (N.pos p)); simpl; auto. |