1 files changed, 2 insertions, 6 deletions
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