diff --git a/src/kernel_services/abstract_interp/eva_lattice_type.mli b/src/kernel_services/abstract_interp/eva_lattice_type.mli index 99d58f9ed1bd19c2ece2f1c1ceb85384c002787b..4846df09c3c04eeb3d24de09fc3de0e3a0c815a6 100644 --- a/src/kernel_services/abstract_interp/eva_lattice_type.mli +++ b/src/kernel_services/abstract_interp/eva_lattice_type.mli @@ -55,7 +55,7 @@ end module type With_Diff_One = sig type t val diff_if_one : t -> t -> t or_bottom - (** [diff_of_one t1 t2] is an over-approximation of [t1-t2]. + (** [diff_if_one t1 t2] is an over-approximation of [t1-t2]. @return [t1] if [t2] is not a singleton. *) end diff --git a/src/kernel_services/abstract_interp/lattice_type.mli b/src/kernel_services/abstract_interp/lattice_type.mli index a494ea5ea67ac6c910bc95c9f441970c807a1f72..3bcc722d23a98f8633a211d3204fab2056e8c010 100644 --- a/src/kernel_services/abstract_interp/lattice_type.mli +++ b/src/kernel_services/abstract_interp/lattice_type.mli @@ -105,7 +105,7 @@ end module type With_Diff_One = sig type t val diff_if_one : t -> t -> t - (** [diff_of_one t1 t2] is an over-approximation of [t1-t2]. + (** [diff_if_one t1 t2] is an over-approximation of [t1-t2]. @return [t1] if [t2] is not a singleton. *) end