The files `Coq.Numbers.Integer.Abstract.ZDivEucl`

and `Coq.Zarith.Zeuclid`

deal with "euclidean division" in Z, that is division with a nonnegative remainder.

This choice (among 2 others) is discussed, as said in the Coq doc in this article.

Since it's not one of the two choices (floor division and truncation division) in `ZArith.BinInt`

, I think we should deprecate it for simplification.

What do you think?

I propose deprecation here : https://github.com/coq/coq/pull/18544

Please, do not hesitate to comment and/or object.

Last updated: Oct 13 2024 at 01:02 UTC