From b389b6e3b6754f9f12190bfd2c0e7f68783b582f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Mon, 20 Jan 2020 15:55:13 +0100 Subject: [zify] efficiency improvements - zify_iter_specs is entirely in OCaml - zify_op has been improved * The generation of proof-terms is more direct * It does not `rewrite` but instead either performs a `pose proof` or a `change` * The support for `and`, `or`, `not`, arrow is hardcoded * Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x - zify_elim_let is entirely in OCaml (no Ltac callback) [micromega] fix stack overflow Less naive computation of bounds (online elimination of duplicates) --- doc/changelog/04-tactics/11429-zify-optimisation.rst | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 doc/changelog/04-tactics/11429-zify-optimisation.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst new file mode 100644 index 0000000000..ce5bfa4aad --- /dev/null +++ b/doc/changelog/04-tactics/11429-zify-optimisation.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `zify` by rewritting the remaining Ltac code in OCaml. + (`#11429 `_, by Frédéric Besson). -- cgit v1.2.3