From 74d7dd7ae08dedfd80c056a345c1b3398eb91b5e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 22 Apr 2015 17:39:42 +0200
Subject: Pp: obsolete comment.

Was made incorrect by 98a710caf5e907344329ee9e9f7b5fd87c50836f .---
 lib/pp.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index e8b42ed797..6e6b32c590 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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
-- 
cgit v1.2.3