4 files changed, 13 insertions, 3 deletions
diff --git a/lib/bigint.ml b/lib/bigint.ml
index e95604ffc0..1ecc2ce2cc 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -257,9 +257,9 @@ let sub_mult m d q k =
     end
   done
 
-(** Euclid division m/d = (q,r)
-    This is the "Floor" variant, as with ocaml's /
-    (but not as ocaml's Big_int.quomod_big_int).
+(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|.
+    This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"),
+    as with ocaml's / (but not as ocaml's Big_int.quomod_big_int).
     We have sign r = sign m *)
 
 let euclid m d =
diff --git a/lib/bigint.mli b/lib/bigint.mli
index e5525f164e..a1dc660771 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -30,6 +30,12 @@ val mult_2 : bigint -> bigint
 val add : bigint -> bigint -> bigint
 val sub : bigint -> bigint -> bigint
 val mult : bigint -> bigint -> bigint
+
+(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|.
+    This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"),
+    as with ocaml's / (but not as ocaml's Big_int.quomod_big_int).
+    We have sign r = sign m *)
+
 val euclid : bigint -> bigint -> bigint * bigint
 
 val less_than : bigint -> bigint -> bool
diff --git a/lib/util.ml b/lib/util.ml
index 0d2425f271..36282b2dac 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -136,6 +136,8 @@ type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
 
+let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
+
 module Union =
 struct
   let map f g = function
diff --git a/lib/util.mli b/lib/util.mli
index cf8041a0d9..56ec5394eb 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -133,5 +133,7 @@ type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 
 type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
 
+val sym : ('a, 'b) eq -> ('b, 'a) eq
+
 val open_utf8_file_in : string -> in_channel
 (** Open an utf-8 encoded file and skip the byte-order mark if any. *)