From 83f05bf19970b5e75f9e23a80d7229f185b74ade Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 2 May 2014 22:40:17 +0200
Subject: [PATCH] Update copyright headers.

---
 theories/ars.v             | 2 +-
 theories/assoc.v           | 2 +-
 theories/base.v            | 2 +-
 theories/collections.v     | 2 +-
 theories/countable.v       | 2 ++
 theories/decidable.v       | 2 +-
 theories/fin_collections.v | 2 +-
 theories/fin_map_dom.v     | 2 +-
 theories/fin_maps.v        | 2 +-
 theories/finite.v          | 2 ++
 theories/fresh_numbers.v   | 2 +-
 theories/lexico.v          | 2 +-
 theories/list.v            | 2 +-
 theories/listset.v         | 2 +-
 theories/listset_nodup.v   | 2 +-
 theories/map.v             | 2 +-
 theories/mapset.v          | 2 +-
 theories/natmap.v          | 2 +-
 theories/nmap.v            | 2 +-
 theories/numbers.v         | 2 +-
 theories/option.v          | 2 +-
 theories/orders.v          | 2 +-
 theories/pmap.v            | 2 +-
 theories/prelude.v         | 2 +-
 theories/proof_irrel.v     | 2 +-
 theories/tactics.v         | 2 +-
 theories/vector.v          | 2 +-
 theories/zmap.v            | 2 +-
 28 files changed, 30 insertions(+), 26 deletions(-)

diff --git a/theories/ars.v b/theories/ars.v
index 7bbe16d3..5b15d13f 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 60c4e8c8..37dc2f90 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 d6b470dc..7064c776 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 79d39ae3..61a73598 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 1ea69bda..73b5ff72 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 778be133..e58ef199 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 b6898dd5..934413d4 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 431f7604..c081ee5f 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 57be9f1f..e6d02d54 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 75cbd9db..4bcaa09f 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 1e8c5d85..88723303 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 1339db21..6b07fefa 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 f416e5b1..b4ae91c2 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 42b3971d..225034b9 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 b7c5ddf9..2e9275eb 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 14ac9cfc..89350a68 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 113f2478..ae5741e5 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 236a62f2..b0b44f74 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 a33fb8a6..2528e70f 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 0fea1590..9ac7c50f 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 384d9e3f..1fdfc80b 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 4e6b6e0c..f63f5b11 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 800bfe16..a58393bd 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 a0e6f2bf..61b9689a 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 56cd5340..77b7c2c4 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 a15dc055..04111e47 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 f54d1840..2583758b 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 7c75dea7..52dc4fd0 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]. *)
-- 
GitLab