From 64a5f8f4e803971eac858a2f1dbb748c681fa5ed Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 13 Nov 2019 22:18:20 +0900 Subject: Update doc/changelog/04-tactics/10998-zify-complements.rst Co-Authored-By: Théo Zimmermann --- doc/changelog/04-tactics/10998-zify-complements.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 `_, by Kazuhiko Sakaguchi). -- cgit v1.2.3