From 7bf884b7c525092db74ac2effcf1091bd3c3d46c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 Sep 2020 18:23:55 +0200
Subject: [zarith] [micromega] Bump to 1.10 and remove some hacks

In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in
1.10, see

https://github.com/ocaml/Zarith/issues/58
---
 plugins/micromega/numCompat.mli | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'plugins/micromega/numCompat.mli')

diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..fe0a6e7660 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
 
-- 
cgit v1.2.3


From acb24a1540c33f075a83f9788614e5c2f3335b0a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 14 Sep 2020 18:26:21 +0200
Subject: [micromega] Use `minus_one` built-in zarith constant.

---
 plugins/micromega/numCompat.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/micromega/numCompat.mli')

diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index fe0a6e7660..0b4d52708f 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -47,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
-- 
cgit v1.2.3