diff options
| author | Kazuhiko Sakaguchi | 2019-11-13 22:18:20 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-11-15 14:20:21 +0900 |
| commit | 64a5f8f4e803971eac858a2f1dbb748c681fa5ed (patch) | |
| tree | 96fd875247abc7277d9b99d5e2a0b04869bbd40f | |
| parent | f9312f45b386c33723c0ec7741556e9389639f2c (diff) | |
Update doc/changelog/04-tactics/10998-zify-complements.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
| -rw-r--r-- | doc/changelog/04-tactics/10998-zify-complements.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst index e0632e3f74..3ec526f0a9 100644 --- a/doc/changelog/04-tactics/10998-zify-complements.rst +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -1,7 +1,7 @@ - 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 `ZifyBool.v` (`isZero` and `isLeZero`) + Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`) are also added to help users to declare new :tacn:`zify` class instances using Micromega tactics. (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi). |