diff --git a/headers/library-header b/headers/library-header
new file mode 100644
index 0000000000000000000000000000000000000000..af67a93b56a3df7edb0755f880d6ee0e653504bb
--- /dev/null
+++ b/headers/library-header
@@ -0,0 +1,7 @@
+
+ Feat
+
+ François Pottier, Inria Paris
+
+Copyright Inria. All rights reserved. This file is distributed under the
+terms of the MIT license, as described in the file LICENSE.
diff --git a/src/Enum.ml b/src/Enum.ml
index 2a853dcafc052b72315f7dcc99016d5183e1a5cc..89809c0b21fcf9f2e4542c394c14725b7f7b40f5 100644
--- a/src/Enum.ml
+++ b/src/Enum.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* -------------------------------------------------------------------------- *)
(* Core combinators. *)
diff --git a/src/Enum.mli b/src/Enum.mli
index 4ce7f00fd5c36ece99528ff01c9c5b9af0caf731..0b16b75445edbf9fb357596e4c160e907f78b7de 100644
--- a/src/Enum.mli
+++ b/src/Enum.mli
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* An enumeration of type ['a enum] can be loosely thought of as a set of
values of type ['a], equipped with a notion of size. More precisely, it
is a function of a size [s] to a subset of inhabitants of size [s],
diff --git a/src/IFSeq.ml b/src/IFSeq.ml
index b8deaeaf10495be43ce9ff3cac31b506c5b0b463..cd2175396c53aaba051059509f7729e2ba8c4fed 100644
--- a/src/IFSeq.ml
+++ b/src/IFSeq.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* The default implementation of the signature SEQ is based on IFSeqSyn,
instantiated with the unbounded integers provided by [zarith]. *)
diff --git a/src/IFSeq.mli b/src/IFSeq.mli
index 8300bbe74db09e04f69c9e6deb35316ac7e437e7..d0c0cfff2bb9e090b4c98928e077f8641bef8743 100644
--- a/src/IFSeq.mli
+++ b/src/IFSeq.mli
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
open IFSeqSig
(* An implementation of the signature SEQ,
diff --git a/src/IFSeqList.ml b/src/IFSeqList.ml
index d473dc36e049a24278f181255f1b137f4bc15b8f..988bde987518c950a80d5880ac86d065047aa3d8 100644
--- a/src/IFSeqList.ml
+++ b/src/IFSeqList.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* No need to use unbounded integers here, since we will run out of time and
memory before an overflow occurs. *)
diff --git a/src/IFSeqList.mli b/src/IFSeqList.mli
index 3f57d42812279520bb0d11b480da39677520e129..b4fd392c4d9a5dd01ad8a262838541ae0be430f2 100644
--- a/src/IFSeqList.mli
+++ b/src/IFSeqList.mli
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* This is a naive implementation of finite sequences as lists. *)
open IFSeqSig
diff --git a/src/IFSeqObj.ml b/src/IFSeqObj.ml
index 8900bdfe92057ed00e6e2a3ade9b5dc4e9218bfb..6e8133c40255c2a0b4624ad97834999143975f46 100644
--- a/src/IFSeqObj.ml
+++ b/src/IFSeqObj.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* This is an implementation of implicit finite sequences as objects, that is,
records of closures. This is the implementation style proposed in the Feat
paper by Duregard et al. *)
diff --git a/src/IFSeqObj.mli b/src/IFSeqObj.mli
index 4b3285939c7c31d623e6100b6ef66fdd1e3663a4..661f8e41fe948a985355cc6893cddd16ffe0a883 100644
--- a/src/IFSeqObj.mli
+++ b/src/IFSeqObj.mli
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
open IFSeqSig
(* This is an implementation of implicit finite sequences as objects, that is,
diff --git a/src/IFSeqSig.ml b/src/IFSeqSig.ml
index d66f1423fcd039a11c77628761b94129b300c062..4462569309c352cea8fbf6dd9540c7b848b8c184 100644
--- a/src/IFSeqSig.ml
+++ b/src/IFSeqSig.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* A signature for implicit finite sequences. *)
(* These sequences are implicit, which means that they are not explicitly
diff --git a/src/IFSeqSyn.ml b/src/IFSeqSyn.ml
index ed4599c898aa23d0d9f3f57350359790076d60dd..f01df7952193581609a8ad24eb3b06c913562bd3 100644
--- a/src/IFSeqSyn.ml
+++ b/src/IFSeqSyn.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* This is an implementation of implicit finite sequences as syntax, that is,
algebraic data structures. This style should be more efficient than the one
used in IFSeqObj, because fewer memory blocks are allocated (one block per
diff --git a/src/IFSeqSyn.mli b/src/IFSeqSyn.mli
index b2dd3c49a1178383a7d029c2416d2728d5a0277f..81a4c57ff9fe67c02cd51e0e942de73aeef00625 100644
--- a/src/IFSeqSyn.mli
+++ b/src/IFSeqSyn.mli
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
open IFSeqSig
(* This is an implementation of implicit finite sequences as syntax,
diff --git a/src/bigint.ml b/src/bigint.ml
index 52abbe8f3647d2613389f5579ada7dbdaa27b6ab..e1ccd36f47d776185daf4877465dea62d64fab76 100644
--- a/src/bigint.ml
+++ b/src/bigint.ml
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* Uniform random generation of large integers. Copied and adapted from Jane
Street's bignum library. *)
diff --git a/src/bigint.mli b/src/bigint.mli
index b90a2e60887d62713f57127857aa1fd92a67c407..b1358ee058c4c7493def9df99ae85e6a44bcf6e2 100644
--- a/src/bigint.mli
+++ b/src/bigint.mli
@@ -1,3 +1,13 @@
+(******************************************************************************)
+(* *)
+(* Feat *)
+(* *)
+(* François Pottier, Inria Paris *)
+(* *)
+(* Copyright Inria. All rights reserved. This file is distributed under the *)
+(* terms of the MIT license, as described in the file LICENSE. *)
+(******************************************************************************)
+
(* Uniform random generation of large integers. *)
val random: Z.t -> Z.t