diff options
| author | Gaëtan Gilbert | 2018-09-04 13:25:05 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-04 13:25:05 +0200 |
| commit | 6d14f27dc75c68d9964755540ae795332eac3844 (patch) | |
| tree | 65216e45f8f2ee5fa9e30be4f356d2f6d4ebaac0 /clib | |
| parent | b40d68fa4fc07a9b585dbd602e94224d6b3f2a7a (diff) | |
| parent | 5cc3e117ed0264e35a46b6e3bb416b4b7f66b127 (diff) | |
Merge PR #7684: [doc] Build ML API documentation artifact.
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cList.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/clib/cList.mli b/clib/cList.mli index ed468cb977..39d9a5e535 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -289,8 +289,8 @@ sig val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list (** [share_tails l1 l2] returns [(l1',l2',l)] such that [l1] is - [l1'@l] and [l2] is [l2'@l] and [l] is maximal amongst all such - decompositions*) + [l1'\@l] and [l2] is [l2'\@l] and [l] is maximal amongst all such + decompositions *) (** {6 Association lists} *) |