diff --git a/feat/Enum.mli b/feat/Enum.mli
index ec0de7c9500dafcc0a4dc60aed6096a4c50095c1..58caf9856238b6311c4684556d9812b47ea614b7 100644
--- a/feat/Enum.mli
+++ b/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
diff --git a/feat/IFSeq.mli b/feat/IFSeq.mli
index 0ae02c5d71a7da9444ad79f2d9cc46abe9374282..570d6dbb15ef4d5c8fa9aff9b7b53bedf37f9716 100644
--- a/feat/IFSeq.mli
+++ b/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
diff --git a/feat/Num.mli b/feat/Num.mli
index 4c771fce39b2f78447a25061e2b63d52bbf9c1e0..2f8e4562ed161bd53cc21fe6648d96208f7efcc5 100644
--- a/feat/Num.mli
+++ b/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