diff --git a/src/kernel_services/analysis/filter/field.ml b/src/kernel_services/analysis/filter/field.ml index df7371741791a4f00d7aed11c33fa90fd0876740..d7b53d09c64e66c0cae29340445818ce99432278 100644 --- a/src/kernel_services/analysis/filter/field.ml +++ b/src/kernel_services/analysis/filter/field.ml @@ -38,7 +38,7 @@ module type S = sig val max : scalar -> scalar -> scalar val min : scalar -> scalar -> scalar - val ( == ) : scalar -> scalar -> bool + val ( = ) : scalar -> scalar -> bool val ( <= ) : scalar -> scalar -> bool val ( < ) : scalar -> scalar -> bool val ( >= ) : scalar -> scalar -> bool diff --git a/src/kernel_services/analysis/filter/finite.ml b/src/kernel_services/analysis/filter/finite.ml index e80796ae2451afb447d8ded1cfa6dae1640609eb..5ad748ccb5b87567fa4873018fdb253737ef591f 100644 --- a/src/kernel_services/analysis/filter/finite.ml +++ b/src/kernel_services/analysis/filter/finite.ml @@ -24,9 +24,9 @@ open Nat type 'n finite = int -let first : type n. n succ finite = 0 -let next : type n. n finite -> n succ finite = fun n -> n + 1 -let ( == ) : type n. n finite -> n finite -> bool = fun l r -> l = r +let first : type n. n succ finite = 0 +let next : type n. n finite -> n succ finite = fun n -> n + 1 +let ( = ) : type n. n finite -> n finite -> bool = fun l r -> l = r let to_int : type n. n finite -> int = fun n -> n let of_int : type n. n succ nat -> int -> n succ finite option = diff --git a/src/kernel_services/analysis/filter/finite.mli b/src/kernel_services/analysis/filter/finite.mli index 007fe137694f5262a72d27a054c3b094c22cf690..28b54b04e5a2a08cc4a92bb16ccfdc845366d5f0 100644 --- a/src/kernel_services/analysis/filter/finite.mli +++ b/src/kernel_services/analysis/filter/finite.mli @@ -25,8 +25,8 @@ open Nat type 'n finite val first : 'n succ finite -val next : 'n finite -> 'n succ finite -val ( == ) : 'n finite -> 'n finite -> bool +val next : 'n finite -> 'n succ finite +val ( = ) : 'n finite -> 'n finite -> bool (* The call [of_int limit n] returns a finite value representing the n-nd element of a finite set of cardinal limit. If n is not in the bounds, none is diff --git a/src/kernel_services/analysis/filter/linear.ml b/src/kernel_services/analysis/filter/linear.ml index 72df26f0c6e5a3e7ecce2ad97c492a00cfdab60a..8cd5288d91d9bda27eca4e7494b04e1b062572f9 100644 --- a/src/kernel_services/analysis/filter/linear.ml +++ b/src/kernel_services/analysis/filter/linear.ml @@ -87,7 +87,7 @@ module Space (Field : Field.S) = struct fun (M m) -> m.rows, m.cols let pretty (type n m) fmt (M m : (n, m) matrix) = - let cut i = if not Finite.(i == first) then Format.pp_print_cut fmt () in + let cut i = if not Finite.(i = first) then Format.pp_print_cut fmt () in let row i = Format.fprintf fmt "@[<h>%a@]" Vector.pretty (row i (M m)) in let pretty () = Finite.for_each (fun i () -> cut i ; row i) m.rows () in Format.pp_open_vbox fmt 0 ; pretty () ; Format.pp_close_box fmt () diff --git a/src/kernel_services/analysis/filter/linear_filter_test.ml b/src/kernel_services/analysis/filter/linear_filter_test.ml index 43e0564ca21f0cbddb37636c58fea7878a072e64..84149c657d9b1bd34d223d23dd502a3b1d234aaf 100644 --- a/src/kernel_services/analysis/filter/linear_filter_test.ml +++ b/src/kernel_services/analysis/filter/linear_filter_test.ml @@ -42,7 +42,7 @@ module Rational = struct let ten = Z.of_int 10 in let sign = if Q.sign n >= 0 then "" else "-" in let num = Q.num n |> Z.abs and den = Q.den n |> Z.abs in - let finish n = Z.Compare.(n >= den || n == Z.zero) in + let finish n = Z.Compare.(n >= den || n = Z.zero) in let rec f e n = if finish n then (n, e) else f (e + 1) Z.(n * ten) in let num, exponent = f 0 num in let default fmt n = Format.fprintf fmt "%1.7f" (Q.to_float n) in @@ -53,7 +53,7 @@ module Rational = struct include Q let infinity = Q.inf - let ( == ) = Q.equal + let ( = ) = Q.equal end