1 files changed, 51 insertions, 34 deletions

diff --git a/lib/predicate.mli b/lib/predicate.mli
index bcc89e72..cee3b0bd 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,67 +1,84 @@
+(** Infinite sets over a chosen [OrderedType].
 
-(** Module [Pred]: sets over infinite ordered types with complement. *)
-
-(** This module implements the set data structure, given a total ordering
-   function over the set elements. All operations over sets
-   are purely applicative (no side-effects).
-   The implementation uses the Set library. *)
+    All operations over sets are purely applicative (no side-effects).
+ *)
 
+(** Input signature of the functor [Make]. *)
 module type OrderedType =
   sig
     type t
-    val compare: t -> t -> int
+    (** The type of the elements in the set.
+
+	The chosen [t] {b must be infinite}. *)
+
+    val compare : t -> t -> int
+    (** A total ordering function over the set elements.
+        This is a two-argument function [f] such that:
+        - [f e1 e2] is zero if the elements [e1] and [e2] are equal,
+        - [f e1 e2] is strictly negative if [e1] is smaller than [e2],
+        - and [f e1 e2] is strictly positive if [e1] is greater than [e2].
+     *)
   end
-          (** The input signature of the functor [Pred.Make].
-             [t] is the type of the set elements.
-             [compare] is a total ordering function over the set elements.
-             This is a two-argument function [f] such that
-             [f e1 e2] is zero if the elements [e1] and [e2] are equal,
-             [f e1 e2] is strictly negative if [e1] is smaller than [e2],
-             and [f e1 e2] is strictly positive if [e1] is greater than [e2].
-             Example: a suitable ordering function is
-             the generic structural comparison function [compare]. *)
 
 module type S =
   sig
     type elt
-          (** The type of the set elements. *)
+    (** The type of the elements in the set. *)
+
     type t
-          (** The type of sets. *)
+    (** The type of sets. *)
+
     val empty: t
-          (** The empty set. *)
+    (** The empty set. *)
+
     val full: t
-          (** The whole type. *)
+    (** The set of all elements (of type [elm]). *)
+
     val is_empty: t -> bool
-        (** Test whether a set is empty or not. *)
+    (** Test whether a set is empty or not. *)
+
     val is_full: t -> bool
-        (** Test whether a set contains the whole type or not. *)
+    (** Test whether a set contains the whole type or not. *)
+
     val mem: elt -> t -> bool
-        (** [mem x s] tests whether [x] belongs to the set [s]. *)
+    (** [mem x s] tests whether [x] belongs to the set [s]. *)
+
     val singleton: elt -> t
-        (** [singleton x] returns the one-element set containing only [x]. *)
+    (** [singleton x] returns the one-element set containing only [x]. *)
+
     val add: elt -> t -> t
-        (** [add x s] returns a set containing all elements of [s],
-           plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
+    (** [add x s] returns a set containing all elements of [s],
+        plus [x]. If [x] was already in [s], then [s] is returned unchanged. *)
+
     val remove: elt -> t -> t
         (** [remove x s] returns a set containing all elements of [s],
-           except [x]. If [x] was not in [s], [s] is returned unchanged. *)
+            except [x]. If [x] was not in [s], then [s] is returned unchanged. *)
+
     val union: t -> t -> t
+    (** Set union. *)
+
     val inter: t -> t -> t
+    (** Set intersection. *)
+
     val diff: t -> t -> t
+    (** Set difference. *)
+
     val complement: t -> t
-        (** Union, intersection, difference and set complement. *)
+    (** Set complement. *)
+
     val equal: t -> t -> bool
-        (** [equal s1 s2] tests whether the sets [s1] and [s2] are
-           equal, that is, contain equal elements. *)
+    (** [equal s1 s2] tests whether the sets [s1] and [s2] are
+        equal, that is, contain equal elements. *)
+
     val subset: t -> t -> bool
         (** [subset s1 s2] tests whether the set [s1] is a subset of
-           the set [s2]. *)
+            the set [s2]. *)
+
     val elements: t -> bool * elt list
         (** Gives a finite representation of the predicate: if the
            boolean is false, then the predicate is given in extension.
            if it is true, then the complement is given *)
   end
 
-module Make(Ord: OrderedType): (S with type elt = Ord.t)
-        (** Functor building an implementation of the set structure
-           given a totally ordered type. *)
+(** The [Make] functor constructs an implementation for any [OrderedType]. *)
+module Make (Ord : OrderedType) : (S with type elt = Ord.t)