diff --git a/theories/ars.v b/theories/ars.v
index 7bbe16d34a02f94c3237dcf32b9b88806821590e..5b15d13fc3cd595fc6824ce3781b9ded0eb07fac 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects definitions and theorems on abstract rewriting systems.
 These are particularly useful as we define the operational semantics as a
diff --git a/theories/assoc.v b/theories/assoc.v
index 60c4e8c84abb542fd0afaafc38dcc6b5a4dabf0a..37dc2f90c521ec814e13de5f571acfc0fbaec9b5 100644
--- a/theories/assoc.v
+++ b/theories/assoc.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** An implementation of finite maps and finite sets using association lists
 ordered by keys. Although the lookup and insert operation are linear-time, the
diff --git a/theories/base.v b/theories/base.v
index d6b470dc2a79d577ef40b102ae357e76ca86a6fd..7064c776235b31314c1273ab99903fcc9151e396 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects type class interfaces, notations, and general theorems
 that are used throughout the whole development. Most importantly it contains
diff --git a/theories/collections.v b/theories/collections.v
index 79d39ae33bd033178770f521fccd611e61ba388e..61a735981db8a34013e82292c13243dbd9a98df0 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects definitions and theorems on collections. Most
 importantly, it implements some tactics to automatically solve goals involving
diff --git a/theories/countable.v b/theories/countable.v
index 1ea69bda5b6d5f946c46ab79c03390207a6d68cf..73b5ff72f4c4d2984bbff1c5fb406252cb2c0a40 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,3 +1,5 @@
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
 Require Export list.
 Local Obligation Tactic := idtac.
 Local Open Scope positive.
diff --git a/theories/decidable.v b/theories/decidable.v
index 778be133b6c6764310ca1c216b1aeae394fc7fd4..e58ef19959c4c0743f5c0d3d4c024df390a1c65c 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects theorems, definitions, tactics, related to propositions
 with a decidable equality. Such propositions are collected by the [Decision]
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index b6898dd54bbde78d09abc57a505206870c22dec7..934413d40d7a431bfdc383a3e465e3285c774cc7 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects definitions and theorems on finite collections. Most
 importantly, it implements a fold and size function and some useful induction
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 431f76048f83db4b04ac01052c5cd3de6e15977c..c081ee5f7309db37b620e79f23e9ad18831f6f4d 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file provides an axiomatization of the domain function of finite
 maps. We provide such an axiomatization, instead of implementing the domain
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 57be9f1f0d14fd30e48eb6c8f7c8c088d6a1570d..e6d02d548ab6b6f6bbbad3072bbfedfa309794d3 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** Finite maps associate data to keys. This file defines an interface for
 finite maps and collects some theory on it. Most importantly, it proves useful
diff --git a/theories/finite.v b/theories/finite.v
index 75cbd9db68952aae48515c3ff08d2072cab1bfdb..4bcaa09f48aa759d0094df6a02a38fb4ae3ca7d7 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,3 +1,5 @@
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
 Require Export countable list.
 Obligation Tactic := idtac.
 
diff --git a/theories/fresh_numbers.v b/theories/fresh_numbers.v
index 1e8c5d85d525c74dded4b577c32f0201421cf02d..88723303069c5d32101d2174ae54f7183fdc6916 100644
--- a/theories/fresh_numbers.v
+++ b/theories/fresh_numbers.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** Given a finite set of binary naturals [N], we generate a fresh element by
 taking the maximum, and adding one to it. We declare this operation as an
diff --git a/theories/lexico.v b/theories/lexico.v
index 1339db21430582db637ae89b32ba8a4d9ea8581a..6b07fefac8ad7e952d088702dc5d372292ef25c5 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This files defines a lexicographic order on various common data structures
 and proves that it is a partial order having a strong variant of trichotomy. *)
diff --git a/theories/list.v b/theories/list.v
index f416e5b110b7b1ac10f368e46a7005accd1696ab..b4ae91c2cbc0fa9edd2efb0b54c6816d9aa50639 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on lists that
 are not in the Coq standard library. *)
diff --git a/theories/listset.v b/theories/listset.v
index 42b3971d2c273a47f0fa52dcedfee989cfd0e5a0..225034b9881570915e1d236cea3fee8d5bc79d7b 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite as unordered lists without duplicates
 removed. This implementation forms a monad. *)
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index b7c5ddf9203f87723ea578aef790d42f283665b1..2e9275eb64da97b625bcc239a9a9f998a004e116 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file implements finite as unordered lists without duplicates.
 Although this implementation is slow, it is very useful as decidable equality
diff --git a/theories/map.v b/theories/map.v
index 14ac9cfc9f308fd6387dcf7afa4db09b73688a89..89350a68b461588e2a9c75a4131ea31abedd5e1c 100644
--- a/theories/map.v
+++ b/theories/map.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 Require Export separation.
 Require Import refinements.
diff --git a/theories/mapset.v b/theories/mapset.v
index 113f2478004cb0b755370d2a39502934a7cb317c..ae5741e56d292497a70ac7ec1179000ff3a01d88 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This files gives an implementation of finite sets using finite maps with
 elements of the unit type. Since maps enjoy extensional equality, the
diff --git a/theories/natmap.v b/theories/natmap.v
index 236a62f258f7e0a099610d3a8d05f59198465041..b0b44f74d25ba4c129676e2de0608f5cf8761367 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This files implements a type [natmap A] of finite maps whose keys range
 over Coq's data type of unary natural numbers [nat]. The implementation equips
diff --git a/theories/nmap.v b/theories/nmap.v
index a33fb8a6efd6a27f10954e4102d75b473497c932..2528e70f4664fd7b6f5da5ea2a36d367c29412f4 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This files extends the implementation of finite over [positive] to finite
 maps whose keys range over Coq's data type of binary naturals [N]. *)
diff --git a/theories/numbers.v b/theories/numbers.v
index 0fea15900c25a923b3ce9f699b2eb99f14c0e8eb..9ac7c50f8282961e0e341cf23db1b4c565761057 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects some trivial facts on the Coq types [nat] and [N] for
 natural numbers, and the type [Z] for integers. It also declares some useful
diff --git a/theories/option.v b/theories/option.v
index 384d9e3f45d178bb9af7d91d6e06aec48baeefb9..1fdfc80bab32898ac40e211553b3001e56136438 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
diff --git a/theories/orders.v b/theories/orders.v
index 4e6b6e0c57c8a1ca9c4b66599c3969483d5308de..f63f5b11cd6a223005b508d3868e5513fb547731 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects common properties of pre-orders and semi lattices. This
 theory will mainly be used for the theory on collections and finite maps. *)
diff --git a/theories/pmap.v b/theories/pmap.v
index 800bfe1680746d4d2906128ef0d60e6173f22a42..a58393bd8270d665937120ebc2be523b7faa3ee9 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This files implements an efficient implementation of finite maps whose keys
 range over Coq's data type of positive binary naturals [positive]. The
diff --git a/theories/prelude.v b/theories/prelude.v
index a0e6f2bfe4297d07cedb49c9364d0f5892e225c2..61b9689a37d9f5b1b698b0b0ab5b9aa7b2b93d68 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 Require Export
   base
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 56cd5340838942ff529960dc12cf559b4a76d25d..77b7c2c485d79bcc7f3097a1e2454e34de1d77e8 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects facts on proof irrelevant types/propositions. *)
 Require Export Eqdep_dec tactics.
diff --git a/theories/tactics.v b/theories/tactics.v
index a15dc055350493b1f1a01e95603f1e92dbbebd5d..04111e478d8c2a39d08b69563636eda5760f44ae 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose tactics that are used throughout
 the development. *)
diff --git a/theories/vector.v b/theories/vector.v
index f54d184008894608a0cda839b0c46d6555a3005d..2583758bdbe5ea3a8f843781b5298b1e726bf01d 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on vectors
 (lists of fixed length) and the fin type (bounded naturals). It uses the
diff --git a/theories/zmap.v b/theories/zmap.v
index 7c75dea789a466d4df46ec85267a1a74bbe8e275..52dc4fd0c1449d0750a4d62a30342466cdfdbbb2 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2013, Robbert Krebbers. *)
+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
 (** This files extends the implementation of finite over [positive] to finite
 maps whose keys range over Coq's data type of binary naturals [Z]. *)