aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-10 09:45:21 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-06-10 09:45:21 +0200
commita19746f2ff7933f0b78ecfcd78e3237ef721977a (patch)
tree6e2bb24cac2f4d9efe589507810b2558d5cbd0d6
parent51a56b1aacb516af513de64c00dd7e796f661484 (diff)
[lib] Fix wrong deprecation comment.
-rw-r--r--clib/cList.ml1
-rw-r--r--clib/cList.mli2
2 files changed, 2 insertions, 1 deletions
diff --git a/clib/cList.ml b/clib/cList.ml
index 646e39d23..2b627f745 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -116,6 +116,7 @@ sig
val subtract : 'a eq -> 'a list -> 'a list -> 'a list
val subtractq : 'a list -> 'a list -> 'a list
val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+ [@@ocaml.deprecated "Same as [merge_set]"]
val distinct : 'a list -> bool
val distinct_f : 'a cmp -> 'a list -> bool
val duplicates : 'a eq -> 'a list -> 'a list
diff --git a/clib/cList.mli b/clib/cList.mli
index d080ebca2..13e069e94 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -354,7 +354,7 @@ sig
(** [subtract] specialized to physical equality *)
val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
- (** [@@ocaml.deprecated "Same as [merge_set]"] *)
+ [@@ocaml.deprecated "Same as [merge_set]"]
(** {6 Uniqueness and duplication} *)