Merge PR #10046: [primitive integers] Make div21 implems consistent with its specification

Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
Ack-by: proux01
Reviewed-by: vbgl

1 files changed, 4 insertions, 0 deletions

diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index b5f40ca804..f25f24512d 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -40,6 +40,10 @@ val rem     : t -> t -> t
       (* Specific arithmetic operations *)
 val mulc    : t -> t -> t * t
 val addmuldiv : t -> t -> t -> t
+
+(** [div21 xh xl y] returns [q % 2^63, r]
+    s.t. [xh * 2^63 + xl = q * y + r] and [r < y].
+    When [y] is [0], returns [0, 0]. *)
 val div21   : t -> t -> t -> t * t
 
       (* comparison *)