diff --git a/theories/base.v b/theories/base.v
index 264ecfc096231d502d15fa76b316ad26886c9d11..c16f05c9f26c79eb09d32b6a35545de874b61684 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/bset.v b/theories/bset.v
index f0b7a05037b75f08b6fc4462440d57c814b681eb..ffb599f1db4dc5cae590aaa3c014b49d1c81f93b 100644
--- a/theories/bset.v
+++ b/theories/bset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
From stdpp Require Export prelude.
diff --git a/theories/coPset.v b/theories/coPset.v
index 6c45429d199bd6cba60f9ad9d28140428dd4585e..f0a8f51656e9f48bb6f32b3e3781a0181851958b 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/collections.v b/theories/collections.v
index 68bef149c753f3db7f5f56d0766b2533a7968bae..170507b0025cd4921e2060936f4f2ffcae50e196 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 9e3a47e51cb601dcc2c045b3316f61d41fdaeb2d..4619d73b8a5e60cbdab1299ed462c1f66f173281 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From Coq.QArith Require Import QArith_base Qcanon.
From stdpp Require Export list numbers.
diff --git a/theories/decidable.v b/theories/decidable.v
index 1f51743866bb376973efa8cdc7b2c842c5797367..c78d72a6f01edf12d7d3fb1f47eeb2ea9fa7acdf 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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.v b/theories/fin.v
index 6dc71b127a3effe1b7fe9fd993492376bc2061c9..09cfee2e8bda62d0f903e869bfdc1e4e1dc01eff 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the fin type
(bounded naturals). It uses the definitions from the standard library, but
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 2986600e1fa8e2915fc6e05b652388bab4c749fb..aaf08653c54ff6e8e79d56dd2ef2eaf1ec45a989 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 a76c707623ed5c9a2ba9770b0059a793e2eddb45..761dd4baab781643d7da32e8e1c09e20b81d31bc 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 9d093967275239cbd99a481cbefab8a6b9894b84..fc3d6840c844e5b378eedd72203b1ceb92cce4db 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 16f728e01bc48b5a0432144bc3f591ffb544a73e..c5013d7695120df74278a06a1aad282dd4f6389c 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export countable vector.
Set Default Proof Using "Type".
diff --git a/theories/functions.v b/theories/functions.v
index cbf5cd3c94f4b89924cc2016b4912a11a46ce751..2c28b1f5e29af40b5ba81d5d5bf1edc70378e26b 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export base tactics.
Set Default Proof Using "Type".
diff --git a/theories/gmap.v b/theories/gmap.v
index d9f751b7ddb40d4b96bb56ad7b24ab7f7d6d434f..93b85b6d67940755a4d36f73fd09e812fbfbc169 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/gmultiset.v b/theories/gmultiset.v
index 71ab27658bd685b5ab185a8e26e8e133d560486f..8af0dec025840f181366e83b3db7d47ac0c99eb4 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import gmap.
Set Default Proof Using "Type".
diff --git a/theories/hashset.v b/theories/hashset.v
index 20a7d4ae07c1507310e459cdfa5cd8c0ebc53d52..48dd2ec71cf837d0c3816f7dcee94d94aa659f25 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/hlist.v b/theories/hlist.v
index 046a419d7eeeedd814f8298d50eb3e0b2a64d5ec..3f845e9fee45729ade7e5a366ff2a33e3cb66a0f 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import tactics.
Set Default Proof Using "Type".
diff --git a/theories/infinite.v b/theories/infinite.v
index e5c5ceb3edf5102958af7fe191017d6c2df7f1b8..b136f43b42952e6e29246ed6a83ec75f78092b52 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Import pretty fin_collections relations prelude gmap.
diff --git a/theories/lexico.v b/theories/lexico.v
index adcc072daf361f81dc7f296b5992d9cfd3d8bcb5..c045e5e9910bcf3be7dc3f56be47a58a466c8812 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 60cded9e99c67d2e993d8082230c40c6470fe3dd..f1e5b42bc8c43c8af2d1f2cf318d115567806678 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 824cbc4513a873ad720018ca11c29baf92cc3f12..23ac7c389a7780175bd6a1344908f5e3e80721a2 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 dbfb2d62ad28b5937f4bfe22e98aaeb5cb51a8ca..a4835acaac8a2149bea0d42cc8bf5a6240a5ee27 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 7a497ccb669b0a516777886cf0ebec420fce7cfa..bb60accbbe0220baf72d4111843639aac1ebf973 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 daa00e46668006913c7e85fc8e0961c902af089b..bc68edd6e8bb629889fd692998b0a86e465292c6 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 7e56c562ad7b5db69bb5e1937a6526afb5ff3aab..bbdc1c6e71c71a199730b2c59dec3cab65b26f09 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 4422e619c5326c3007e5eb535967f6a9c876be46..1ef1721ddd46155855e4609993f6b68930fdf329 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 52abba338ea30f4a099856e48d9c71ebbd04fedb..7900d9db784d7e258c386680126bd6151d817ca0 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 b7fc6948705a38ea62ba103046eb8170db1cc500..db754409da8e02111df140a9b28d4d4968fa3285 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/pmap.v b/theories/pmap.v
index 1a35e6d1fcda713514512890c9199c8de28a642f..db46a61093cd2c9617b96803ccd0e29489200b94 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 b62ce668af59c469e28805d9bca78337734e2806..fc2ea9d3cc23426ee7cf1413c6b80ccf717d5824 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export
base
diff --git a/theories/pretty.v b/theories/pretty.v
index c879e43e4bdeefb604eeb1febce0accf41bb9408..2d8c863512e5e9307a8907285e4ae78a33e8c5f1 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export strings.
From stdpp Require Import relations numbers.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 0ca5e4e30edf19557881796233e36cd10e2ecbd4..9c442e6dc6f7c4faab6b5e2558f01bc8674dcdd2 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
From stdpp Require Export base.
diff --git a/theories/relations.v b/theories/relations.v
index 30dd4d66d45af8b74b79956bf665a7a77f701f5a..df9657edc86446704e582de8bdd16f1e59e281e5 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/set.v b/theories/set.v
index 235900ea4257df136f60f4e2feec5bab5f6bf1b1..a823d705526d0bb1f8a9c4e519cc39c6126138a1 100644
--- a/theories/set.v
+++ b/theories/set.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
From stdpp Require Export collections.
diff --git a/theories/sorting.v b/theories/sorting.v
index 9576fdbc145b8c9ea35ebf23d01b49c8072e34d0..f29e7b2811f7b620f3661d6ebe25c8bdf1fc6f54 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/streams.v b/theories/streams.v
index d4e610d50d3d266b8c0b0c9bc1fcf84e92538907..2880a9a9c185c9ab2efcdfd672d19816938766cb 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export tactics.
Set Default Proof Using "Type".
diff --git a/theories/stringmap.v b/theories/stringmap.v
index 14fffc9671751490e9d484267e0ac3202a18de78..d8866474723d4e765796edaee9390d02f58d6de2 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/strings.v b/theories/strings.v
index 2110270a720d7e11135b716955b188caaf538d69..7c674d38ab38e54839a4c5572c595e96391b1e47 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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/tactics.v b/theories/tactics.v
index fd420dda03d74f01f439cbfc1d2ff0a251ca2b33..51df63830261e1ccf861feae62286ded1afcfbb5 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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 e46774e74e5570251a5b0d4ff9e0a88daa88732b..3607efbe1473a54aa8e11bbba0652dfcbcd2629d 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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). It uses the definitions from the standard library, but
diff --git a/theories/zmap.v b/theories/zmap.v
index 31177c02e0b52170ca2d8b3d848e383f34b82ed9..d4f015b50be22aeb36788821260434d93bba191c 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -1,4 +1,4 @@
-(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* Copyright (c) 2012-2019, Coq-std++ developers. *)
(* 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]. *)