Merge PR #8743: [micromega] Switch from `Big_int` to ZArith.

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: fajb
Ack-by: liyishuai
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: soraros
Ack-by: thery
Ack-by: vbgl

1 files changed, 10 insertions, 1 deletions

diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..0b4d52708f 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -25,8 +25,15 @@ module type ZArith = sig
   val power_int : t -> int -> t
   val quomod : t -> t -> t * t
   val ppcm : t -> t -> t
+
+  (** [gcd x y] Greatest Common Divisor. Must always return a
+     positive number *)
   val gcd : t -> t -> t
+
+  (** [lcm x y] Least Common Multiplier. Must always return a
+     positive number *)
   val lcm : t -> t -> t
+
   val to_string : t -> string
 end
 
@@ -40,7 +47,9 @@ module type QArith = sig
   val one : t
   val two : t
   val ten : t
-  val neg_one : t
+
+  (** -1 constant  *)
+  val minus_one : t
 
   module Notations : sig
     val ( // ) : t -> t -> t