From 98a61f434c9123f02830182b58935de416627c0e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 18 Mar 2020 16:50:36 +0100
Subject: Reduce the scope of a call to pervasive equality in Coq_micromega.

---
 plugins/micromega/mutils.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins/micromega/mutils.ml')

diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index f9a23751bf..746778cb7c 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -385,7 +385,11 @@ module Hash = struct
   let int_of_eq_op1 =
     Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3)
 
-  let eq_op1 o1 o2 = int_of_eq_op1 o1 = int_of_eq_op1 o2
+  let int_of_eq_op2 =
+    Mc.(function OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)
+
+  let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2)
+  let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2)
   let hash_op1 h o = combine h (int_of_eq_op1 o)
 
   let rec eq_positive p1 p2 =
-- 
cgit v1.2.3


From 1dcd622c45ad8880492d115af9ad8d333a62738e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Mar 2020 12:21:40 +0100
Subject: Fuck off ocamlformat.

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

(limited to 'plugins/micromega/mutils.ml')

diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 746778cb7c..27b917383b 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -386,7 +386,9 @@ module Hash = struct
     Mc.(function Equal -> 0 | NonEqual -> 1 | Strict -> 2 | NonStrict -> 3)
 
   let int_of_eq_op2 =
-    Mc.(function OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)
+    Mc.(
+      function
+      | OpEq -> 0 | OpNEq -> 1 | OpLe -> 2 | OpGe -> 3 | OpLt -> 4 | OpGt -> 5)
 
   let eq_op1 o1 o2 = Int.equal (int_of_eq_op1 o1) (int_of_eq_op1 o2)
   let eq_op2 o1 o2 = Int.equal (int_of_eq_op2 o1) (int_of_eq_op2 o2)
-- 
cgit v1.2.3