@Pierre-Marie Pédrot : as far as I can see there is no Ltac2 integer division, although there is an
Division_by_zero exception. Is this a conscious omission or do I miss something?
If we add this, should we add bit operations as well?
Please do, I think it has been asked several times already.
OK, I will do a PR. Do I have to take something special into account to handle the division by zero?
See PR (https://github.com/coq/coq/pull/15637)
Last updated: Jun 10 2023 at 06:31 UTC