aboutsummaryrefslogtreecommitdiffhomepage
path: root/clib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-11 16:32:08 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-11 16:32:08 +0200
commit47389a133b2cb1ae7c240aa203f018e8a19bdd0d (patch)
treee5d2953b0f2a9adc4b98766d1954eedd9922059b /clib
parent034b70449c094b1b5b022a0596d7639a3b08ca39 (diff)
parenta19746f2ff7933f0b78ecfcd78e3237ef721977a (diff)
Merge PR #7757: [lib] Fix wrong deprecation comment.
Diffstat (limited to 'clib')
-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} *)