diff options
| author | Frédéric Besson | 2019-11-16 14:54:42 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2019-11-16 14:54:42 +0100 |
| commit | 6045fcf7398c4098566f7da5c4cba808c7416788 (patch) | |
| tree | c4cf05c9fe17d6ff456a2de404d65cf70ff95009 /doc | |
| parent | 622b4f3ace40313d8dc17141285da32de80b3183 (diff) | |
| parent | 64a5f8f4e803971eac858a2f1dbb748c681fa5ed (diff) | |
Merge PR #10998: Add missing zify class instances
Ack-by: Zimmi48
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/10998-zify-complements.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst new file mode 100644 index 0000000000..3ec526f0a9 --- /dev/null +++ b/doc/changelog/04-tactics/10998-zify-complements.rst @@ -0,0 +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 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). |