diff options
Diffstat (limited to 'doc/changelog/04-tactics/10998-zify-complements.rst')
| -rw-r--r-- | doc/changelog/04-tactics/10998-zify-complements.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst index 3ec526f0a9..c72d085687 100644 --- a/doc/changelog/04-tactics/10998-zify-complements.rst +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -1,4 +1,5 @@ -- The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, +- **Added:** + The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`, `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`, `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`. Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`) |