diff --git a/theories/prelude/base.v b/theories/prelude/base.v
index e1c36a0aeb0ef85a6d46a9fe3033a8d54e423823..ccd30423724ba4dc656018139d82d2dc46473776 100644
--- a/theories/prelude/base.v
+++ b/theories/prelude/base.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/bset.v b/theories/prelude/bset.v
index e384b05c5cafeab3ec0fea31e33bb03ba5badcd2..771523039044edb634cb899316f67c9f724cd591 100644
--- a/theories/prelude/bset.v
+++ b/theories/prelude/bset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
From iris.prelude Require Export prelude.
diff --git a/theories/prelude/coPset.v b/theories/prelude/coPset.v
index 63be7ed49f02ccce094f5f964ae078f0df229e5c..b5c11b3b351f2ea16be587c0ff7f431a55c89dd3 100644
--- a/theories/prelude/coPset.v
+++ b/theories/prelude/coPset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files implements the type [coPset] of efficient finite/cofinite sets
of positive binary naturals [positive]. These sets are:
diff --git a/theories/prelude/collections.v b/theories/prelude/collections.v
index 8b3319ee385823657c4150ed12a87c4091dc58cc..2418e485d27c9a6f2b4329aed1e41361132ddfa8 100644
--- a/theories/prelude/collections.v
+++ b/theories/prelude/collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/countable.v b/theories/prelude/countable.v
index ac733dac2ae52dcc65b47ad139b70d0350bc51b1..c99113460dff803f6e60a3ca36061a22378d4ede 100644
--- a/theories/prelude/countable.v
+++ b/theories/prelude/countable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export list.
Set Default Proof Using "Type".
diff --git a/theories/prelude/decidable.v b/theories/prelude/decidable.v
index 95e368550bfe15ef7ae8f58fa859c6b9c1541ca0..74bcbe61eafb7c4b6abc015a60056a177aa54428 100644
--- a/theories/prelude/decidable.v
+++ b/theories/prelude/decidable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/fin_collections.v b/theories/prelude/fin_collections.v
index 5647cdc3399df33cfeccb6cc0cb0698a6cc8b81d..61c4f98f26e64ba19c1e674289aff8af2ac2de1b 100644
--- a/theories/prelude/fin_collections.v
+++ b/theories/prelude/fin_collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/fin_map_dom.v b/theories/prelude/fin_map_dom.v
index 2ab691e22f2702b5e9104bdd1cb8d0e009e9e99b..ba49a38ea1ae83347cf7a3b5ce91cdbd81043c99 100644
--- a/theories/prelude/fin_map_dom.v
+++ b/theories/prelude/fin_map_dom.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/fin_maps.v b/theories/prelude/fin_maps.v
index 159546b8c92089c6d1901f675604a2e8172a6ca6..55dc0fa637f69068d1e96013d2de29daf49fd978 100644
--- a/theories/prelude/fin_maps.v
+++ b/theories/prelude/fin_maps.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/finite.v b/theories/prelude/finite.v
index fbc498a4d224b13d54988902654101ad92109a35..55c7c1e15a3410eaed6e78b80c3c91c9f65dba80 100644
--- a/theories/prelude/finite.v
+++ b/theories/prelude/finite.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export countable vector.
Set Default Proof Using "Type".
diff --git a/theories/prelude/gmap.v b/theories/prelude/gmap.v
index c47984417a43c7a6c32d4ca6b4972461ee765cf5..ea79b8c63517d442620a6a6eac811650e20dcab4 100644
--- a/theories/prelude/gmap.v
+++ b/theories/prelude/gmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
diff --git a/theories/prelude/hashset.v b/theories/prelude/hashset.v
index bfa30fe7cc9cc4911be846761ea8e2a24056b21e..734c42372fda7b5ca00cc3288c098ddfd665d6c6 100644
--- a/theories/prelude/hashset.v
+++ b/theories/prelude/hashset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/lexico.v b/theories/prelude/lexico.v
index 2d836a85ff0d51e1bf354b225d42d0068b2ac264..32db154ea587adebaa3a2c9dfc18748aaff7776f 100644
--- a/theories/prelude/lexico.v
+++ b/theories/prelude/lexico.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/list.v b/theories/prelude/list.v
index 7076f57c4eb919534a38176e909a6884ae4dcf57..b8d72e931a634cb05d096b6c042f4d6c0347af2c 100644
--- a/theories/prelude/list.v
+++ b/theories/prelude/list.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/listset.v b/theories/prelude/listset.v
index 88bda4f61caa1e4b6ecc4d83c2897e11b9d0ed70..9e34359e6c07ed92e8d7ff7d7eb9ee9cbfb42952 100644
--- a/theories/prelude/listset.v
+++ b/theories/prelude/listset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/listset_nodup.v b/theories/prelude/listset_nodup.v
index 960f39b633d206c6a80e439ad558812b7cde730c..8e90b5c6336f70b82f9bf46260d79e7bbc79f9d6 100644
--- a/theories/prelude/listset_nodup.v
+++ b/theories/prelude/listset_nodup.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/mapset.v b/theories/prelude/mapset.v
index 89417c0546aea2180d0711ba0b9e49c6284bf3c6..b141a10c19cf69f2a7c2af087e91ec56b7087023 100644
--- a/theories/prelude/mapset.v
+++ b/theories/prelude/mapset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/natmap.v b/theories/prelude/natmap.v
index 2bf78d1ea612792636be074815d00ad720dc16cb..eb291315992b27a5705794791ada87b0458bea42 100644
--- a/theories/prelude/natmap.v
+++ b/theories/prelude/natmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/nmap.v b/theories/prelude/nmap.v
index 7957b666c861a945b0696540c7f77a354b940486..fb8fe8e380da388af1904b58d0257e591b9c2e04 100644
--- a/theories/prelude/nmap.v
+++ b/theories/prelude/nmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/numbers.v b/theories/prelude/numbers.v
index e26e0e73ad6c596d4ba2b8288b63dfd7ffd91ad0..7094cd0d1556a121930d44c8444137e7ed450398 100644
--- a/theories/prelude/numbers.v
+++ b/theories/prelude/numbers.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/option.v b/theories/prelude/option.v
index 76f72c91299e63b858ae93230ba918a69267e783..ead5bbfee577fb11c418da848a5b13053add2bf5 100644
--- a/theories/prelude/option.v
+++ b/theories/prelude/option.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/orders.v b/theories/prelude/orders.v
index a28f3ed551144154f3751a02a3fb07a92e01b294..5c051ed566ebac32867ea7989205f02bdec47b05 100644
--- a/theories/prelude/orders.v
+++ b/theories/prelude/orders.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use
the relation [⊆] because we often have multiple orders on the same structure *)
diff --git a/theories/prelude/pmap.v b/theories/prelude/pmap.v
index 4d56bc2597318ba73270d7270341a62e213ea121..fc440c838434725f278f63b0a223fae49a6bf6b6 100644
--- a/theories/prelude/pmap.v
+++ b/theories/prelude/pmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude.v b/theories/prelude/prelude.v
index a1cf5343c8d2d6938df992aa0f2e533cce261695..ed52dc05b765c479fae9a62bbc0192d8ab402398 100644
--- a/theories/prelude/prelude.v
+++ b/theories/prelude/prelude.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export
base
diff --git a/theories/prelude/pretty.v b/theories/prelude/pretty.v
index 61dddb24067afa367f3d7734f4346cf66a7b1047..d20573f391034fb37f23b5faac96eeca6292047e 100644
--- a/theories/prelude/pretty.v
+++ b/theories/prelude/pretty.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export strings.
From iris.prelude Require Import relations.
diff --git a/theories/prelude/proof_irrel.v b/theories/prelude/proof_irrel.v
index 6b785c8de6b6b049eca8ab4492ea1f420a53ec21..694ccd8c6f1b563470c6815eb54266c8571e4c7f 100644
--- a/theories/prelude/proof_irrel.v
+++ b/theories/prelude/proof_irrel.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
From iris.prelude Require Export base.
diff --git a/theories/prelude/relations.v b/theories/prelude/relations.v
index 9984fe671d52d66ce63ecfceaca36f4d0bc72ee4..7b2b3f09976fa647c1a52e81c51e5d4b4c4ab062 100644
--- a/theories/prelude/relations.v
+++ b/theories/prelude/relations.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/set.v b/theories/prelude/set.v
index 22e8278f896c31aa0bc4499434bbdda668bfa6ea..7fc9dd5a59f0310001a3890ed516ee8deb834a39 100644
--- a/theories/prelude/set.v
+++ b/theories/prelude/set.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
From iris.prelude Require Export collections.
diff --git a/theories/prelude/sorting.v b/theories/prelude/sorting.v
index 4ae478e012c9ba605449ad86054f07d38d491fcf..709163129e114aa10bab38973ea62aecce99572c 100644
--- a/theories/prelude/sorting.v
+++ b/theories/prelude/sorting.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
standard library, but without using the module system. *)
diff --git a/theories/prelude/streams.v b/theories/prelude/streams.v
index 2b56722d8a1dd92e93b9cb233bfec0836718a91a..9ed4c886fc472d6cc7299deff2894739b2ca0fc2 100644
--- a/theories/prelude/streams.v
+++ b/theories/prelude/streams.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export tactics.
Set Default Proof Using "Type".
diff --git a/theories/prelude/stringmap.v b/theories/prelude/stringmap.v
index 909b65b5b42e130c277ff521d5767582db30c06d..3e6bff39d6a88b2956e1657ef70da5b8f22cb351 100644
--- a/theories/prelude/stringmap.v
+++ b/theories/prelude/stringmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/strings.v b/theories/prelude/strings.v
index 3c72afe6a42b98178888ed23970cd1fecec81b27..100d49461e0b94a7af546ff101e1fdc6c3af7619 100644
--- a/theories/prelude/strings.v
+++ b/theories/prelude/strings.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From Coq Require Import Ascii.
From Coq Require Export String.
diff --git a/theories/prelude/tactics.v b/theories/prelude/tactics.v
index 7133ba584bd8ed403aabff782260220da49d00ef..14086e6b2921dfa1525a28c9824f2c7c8d1ee89d 100644
--- a/theories/prelude/tactics.v
+++ b/theories/prelude/tactics.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/vector.v b/theories/prelude/vector.v
index 4cf8de8a55bf707885736d2451dfcbc89763ca7c..8fe1a843858d78201cbdc68fdb37b8e2ec193bcf 100644
--- a/theories/prelude/vector.v
+++ b/theories/prelude/vector.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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/prelude/zmap.v b/theories/prelude/zmap.v
index cffb198abb1260301add5de05baf941d9228b703..fffde67cc515ccc6dc635f68e39ced1b3814d4e5 100644
--- a/theories/prelude/zmap.v
+++ b/theories/prelude/zmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* Copyright (c) 2012-2017, 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]. *)