diff --git a/theories/ars.v b/theories/ars.v
index 679537badbbc64c5e261a686dc01379152406b80..3b707bf8f121f587ff831ea5311e37f933ea733b 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 370b447b124c318f4d23895d7906506473f9d8ed..e43e1f667024e027ab5c3e5b57e478bbd14778b9 100644
--- a/theories/assoc.v
+++ b/theories/assoc.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 88ad23573bf89873572564136bba357c4c3bc34d..e753fb735d4cfaab2d8cd220161e882dc6c53ab5 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 c3ef61df881c083a85b0d488977c5a9fe66e7234..953b12cfb05d5d64b914672036016e3b566c52f4 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 6ea4690763cd08e82e314801da7418a0a70bc699..42095618d0eb0f29d57c387b1197fd4a324d66d9 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export list.
Local Obligation Tactic := idtac.
diff --git a/theories/decidable.v b/theories/decidable.v
index 2b8821d22e8cf95e8ebe5c729d182bbde5c11e0a..7adf535da1e6083312a22b11281e00d5806eca3f 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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/error.v b/theories/error.v
index 05c36b7bdbd9d8c1476e5c6a91500a612452ef82..1cef6fffd328ce72838e26775a039d402a1d707f 100644
--- a/theories/error.v
+++ b/theories/error.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export list.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 33ad27ecb457fc5f5c870590ccb9eca9f7311bba..0b3789bafd479a4f6be898ae08b35cb84d452b99 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 c081ee5f7309db37b620e79f23e9ad18831f6f4d..ae01fcf4742de84a49ce4033fee49db46b6a6289 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 a3ae2432be17329bdaf5f9db7e3293345f68867d..88f17797fcb30c932290f4b789e75fbd64366605 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 66828c07461ff238f00322a110617e5962747b80..9aa8a459ebe3a1503bd2652bff77136442b7a222 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 88723303069c5d32101d2174ae54f7183fdc6916..27f34b25cf76df2373c043ec452e42da42d94508 100644
--- a/theories/fresh_numbers.v
+++ b/theories/fresh_numbers.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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/hashset.v b/theories/hashset.v
index 26dffddd8a7c9471b6a0487a736f924977993f0c..ca0ba5dd21934b42b10b36cc6a9a6cbce27b045e 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary
diff --git a/theories/lexico.v b/theories/lexico.v
index 6b07fefac8ad7e952d088702dc5d372292ef25c5..e36b552ad473a263aea6638af86e2d73a1d5d6bd 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 8be24df4c8b1d9e577f2ad1f3cd3d1c08494606c..94b468afb54931fd0f01f787c2581a852c297b64 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 1f318c7bf5d4296e075df712ea2ecbbe972b3fde..00872d02efc7058c8ec7d7b32846eeeb5b22dd81 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index b6b6af9a5f177a910abc59af767b3d0bdcb649f7..7328d21ef36a128c008adbe11775367e318934b0 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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/mapset.v b/theories/mapset.v
index 68442e1bd399fc85de3d01d9c0d9c4220a462b4e..4546acc75e4a7141f5cf7546590d31bb250a8154 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 5e134505717f17133db585f445bc80ab56a8967a..4f249931519ae2570dca003a1ba2ad369e72d7f0 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 b66ed43b7d5fedbf54b88b1ac2b0871d120389fb..b6fcf98c321cdd49fb87d8ffe62bd20d8cf59d38 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 ab2ec0ef8c8b055152938f7fcfd36fa0b3c0d652..f0f366a854251d021f7d362eefc8256cfbde17c5 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 c4e6292385009bc834651d03292e7a23c85ff4fd..edb1029374dc8ec101404c25bbb287e04c480fdc 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 5b6da04e34bbd09c3479404d4a352f1f0d90de90..09290008c81d9d831b4e18d03401588752346033 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 2208a9b0e1fc18671430ec4a0ad45f3128aee07c..7bccbf96928cb079e7f89ffa35bbaec957ee922c 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 61b9689a37d9f5b1b698b0b0ab5b9aa7b2b93d68..219e3c9a759d3965244643c5c515c38ff4a8e624 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export
base
diff --git a/theories/pretty.v b/theories/pretty.v
index a8dc87eeb053e1f3aeb0fcaa47398096016a4c75..c5f69c045f190538359b02811cc9dd6141bb743f 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export numbers option.
Require Import Ascii String ars.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 12e2491a6ed23386c8ae1aaa263c3431a15bf9c3..6f065020aaad26eb2ab2e44ed4e0fda43122558a 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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/streams.v b/theories/streams.v
index c39b8ee21c5d692902005f7b29f67a2365d622a8..af231e02f2a693092099986973b685ca499c43c6 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
Require Export tactics.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index 104199a32d627e9eee3b2adc700b484500bc86ec..d14d6f1ba874436d06deca5f835b0f8012a719cc 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 strings [string]. The implementation uses radix-2
diff --git a/theories/tactics.v b/theories/tactics.v
index 63bf802474b37e25cd25a27070d86578ce70d707..88b809b0b947d060ae64d2eaacd8b1e4c54262be 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 f7208fca9bea0b713395f5fa2d00cff1db5d85ce..6cacf063e7d7215aa41658b8fceed1876f63ae0a 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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 b41228d3ae9ac402046a906f1b41b0a06e095c9a..42f15539c86983feb98e25f6f3d8c38c8305ca9e 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* Copyright (c) 2012-2015, 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]. *)