Documentation comments.

feat/Enum.mli

@@ -8,4 +8,10 @@
 (*  terms of the MIT license, as described in the file LICENSE.               *)
 (******************************************************************************)
 
+(**This module offers a concrete data type ['a enum] of {b enumerations} of
+   elements of type ['a]. Suppose that every element of type ['a] is
+   implicitly assigned a certain size. Then, an enumeration is a function of
+   an integer [s] to the (implicit, finite) sequence of all elements whose
+   size is [s]. *)
+
 include FeatCore.EnumSig.ENUM with module IFSeq = IFSeq

feat/IFSeq.mli

@@ -8,4 +8,12 @@
 (*  terms of the MIT license, as described in the file LICENSE.               *)
 (******************************************************************************)
 
+(**This module provides an abstract data type of {b implicit, finite
+   sequences}. An implicit sequence is not explicitly represented in memory
+   as an actual sequence of elements: instead, it is {e described} by a data
+   structure which contains enough information to produce an arbitrary
+   element upon request. This design decision imposes some constraints on
+   the operations that can be efficiently supported: for instance, [filter]
+   is not supported. *)
+
 include FeatCore.IFSeqSig.IFSEQ_EXTENDED with type index = Num.t

feat/Num.mli

@@ -8,6 +8,8 @@
 (*  terms of the MIT license, as described in the file LICENSE.               *)
 (******************************************************************************)
 
+(**This module implements a small set of operations on big integers. *)
+
 (* This module satisfies the signature [BigIntSig.EXTENDED],
    instantiated with unbounded integers from [zarith]. *)
 include FeatCore.BigIntSig.EXTENDED with type t = Z.t