diff options
Diffstat (limited to 'theories/PArith/BinPos.v')
| -rw-r--r-- | theories/PArith/BinPos.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index a30c555c1..0f794c513 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -649,7 +649,7 @@ Theorem sub_mask_carry_spec p q : sub_mask_carry p q = pred_mask (sub_mask p q). Proof. revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl; - try reflexivity; try rewrite IHp; + try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. |