aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/mutils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/mutils.ml')
-rw-r--r--plugins/micromega/mutils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ae89364e6..ce7496fec 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -393,7 +393,7 @@ struct
let from i = i
let next i = i + 1
let pp o i = output_string o (string_of_int i)
- let compare : int -> int -> int = Pervasives.compare
+ let compare : int -> int -> int = Int.compare
end