diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-04-22 17:39:42 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-04-22 18:55:13 +0200 |
commit | 74d7dd7ae08dedfd80c056a345c1b3398eb91b5e (patch) | |
tree | e8f7f71ebe8caccaaed72c89ea3863ff0701cab4 /lib/pp.ml | |
parent | b4552eb74c7ee577339b44924b59c2ab25f893d2 (diff) |
Pp: obsolete comment.
Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 8 |
1 files changed, 2 insertions, 6 deletions
@@ -8,13 +8,9 @@ module Glue : sig - (* A left associative glue implements efficient glue operator - when used as left associative. If glue is denoted ++ then + (** The [Glue] module implements a container data structure with + efficient concatenation. *) - a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @ [a])) - - I.e. if the short list is the second argument - *) type 'a t val atom : 'a -> 'a t |