Merge PR#666: romega revisited : no more normalization trace, cleaned-up resolution trace

2 files changed, 9 insertions, 3 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index e95604ffc..1ecc2ce2c 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 e5525f164..a1dc66077 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