From 22a06f37b55591f3fbb9183b7cd612dad998afe8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 Mar 2020 13:08:02 +0100
Subject: [PATCH] Remove copyright headers, update LICENCE file.
This follows https://gitlab.mpi-sws.org/iris/iris/merge_requests/387
This closes issue #54.
---
LICENSE | 16 +++++++++-------
theories/base.v | 2 --
theories/binders.v | 2 --
theories/boolset.v | 2 --
theories/coGset.v | 2 --
theories/coPset.v | 2 --
theories/countable.v | 2 --
theories/decidable.v | 2 --
theories/fin.v | 2 --
theories/fin_map_dom.v | 2 --
theories/fin_maps.v | 2 --
theories/fin_sets.v | 2 --
theories/finite.v | 2 --
theories/functions.v | 2 --
theories/gmap.v | 2 --
theories/gmultiset.v | 2 --
theories/hashset.v | 2 --
theories/hlist.v | 2 --
theories/infinite.v | 2 --
theories/lexico.v | 2 --
theories/list.v | 2 --
theories/listset.v | 2 --
theories/listset_nodup.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/pretty.v | 2 --
theories/proof_irrel.v | 2 --
theories/propset.v | 2 --
theories/relations.v | 2 --
theories/sets.v | 2 --
theories/sorting.v | 2 --
theories/streams.v | 2 --
theories/stringmap.v | 2 --
theories/strings.v | 2 --
theories/tactics.v | 2 --
theories/vector.v | 2 --
theories/zmap.v | 2 --
43 files changed, 9 insertions(+), 91 deletions(-)
diff --git a/LICENSE b/LICENSE
index 0b9458c2..fafc4105 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,8 @@
All files in this development are distributed under the terms of the BSD
license, included below.
+Copyright: std++ developers and contributors
+
------------------------------------------------------------------------------
BSD LICENCE
@@ -12,18 +14,18 @@ modification, are permitted provided that the following conditions are met:
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
- * Neither the name of the <organization> nor the
- names of its contributors may be used to endorse or promote products
- derived from this software without specific prior written permission.
+ * Neither the name of the copyright holder nor the names of its contributors
+ may be used to endorse or promote products derived from this software
+ without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
-ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/theories/base.v b/theories/base.v
index ce3f7546..0e6fece3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1,5 +1,3 @@
-(* 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
abstract interfaces for ordered structures, sets, and various other data
diff --git a/theories/binders.v b/theories/binders.v
index 3fddac91..995bbdf8 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -1,5 +1,3 @@
-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
(** This file implements a type [binder] with elements [BAnon] for the
anonymous binder, and [BNamed] for named binders. This type is isomorphic to
[option string], but we use a special type so that we can define [BNamed] as
diff --git a/theories/boolset.v b/theories/boolset.v
index 3bfa3b3d..8a0d4c54 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -1,5 +1,3 @@
-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
(** This file implements boolsets as functions into Prop. *)
From stdpp Require Export prelude.
Set Default Proof Using "Type".
diff --git a/theories/coGset.v b/theories/coGset.v
index 84e93102..6736e7ac 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -1,5 +1,3 @@
-(* Copyright (c) 2020, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
(** This file implements the type [coGset A] of finite/cofinite sets
of elements of any countable type [A].
diff --git a/theories/coPset.v b/theories/coPset.v
index 4048edf4..1aefcbe5 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -1,5 +1,3 @@
-(* 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/countable.v b/theories/countable.v
index 4894b0b1..9b5373c4 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -1,5 +1,3 @@
-(* 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.
Set Default Proof Using "Type".
diff --git a/theories/decidable.v b/theories/decidable.v
index 2345ab9f..34f657ad 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -1,5 +1,3 @@
-(* 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]
type class. *)
diff --git a/theories/fin.v b/theories/fin.v
index 905c296d..ab260099 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -1,5 +1,3 @@
-(* 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
renames or changes their notations, so that it becomes more consistent with the
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 5ba8bb78..f061ada1 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -1,5 +1,3 @@
-(* 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
function in a generic way, to allow more efficient implementations. *)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e1c7f17d..f87cc301 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1,5 +1,3 @@
-(* 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
induction principles for finite maps and implements the tactic
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index e71f698a..b91407f4 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -1,5 +1,3 @@
-(* 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 sets. Most
importantly, it implements a fold and size function and some useful induction
principles on finite sets . *)
diff --git a/theories/finite.v b/theories/finite.v
index 1364e274..93292786 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -1,5 +1,3 @@
-(* 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 2c28b1f5..868a430b 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -1,5 +1,3 @@
-(* 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 cd1db448..8684a92c 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -1,5 +1,3 @@
-(* 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. *)
From stdpp Require Export countable infinite fin_maps fin_map_dom.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index aab6bd72..634b010a 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -1,5 +1,3 @@
-(* 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 e0211a16..cb1f86aa 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -1,5 +1,3 @@
-(* 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
integer of type [Z], and contains an unordered list without duplicates. *)
diff --git a/theories/hlist.v b/theories/hlist.v
index 3f845e9f..8f017fdf 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -1,5 +1,3 @@
-(* 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".
Local Set Universe Polymorphism.
diff --git a/theories/infinite.v b/theories/infinite.v
index 232304f6..841e9de2 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -1,5 +1,3 @@
-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export list.
From stdpp Require Import relations pretty.
diff --git a/theories/lexico.v b/theories/lexico.v
index c045e5e9..87106373 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -1,5 +1,3 @@
-(* 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. *)
From stdpp Require Import numbers.
diff --git a/theories/list.v b/theories/list.v
index eb12c9bc..3e7f3553 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1,5 +1,3 @@
-(* 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. *)
From Coq Require Export Permutation.
diff --git a/theories/listset.v b/theories/listset.v
index c692c8ee..c443682b 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,5 +1,3 @@
-(* 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. *)
From stdpp Require Export sets list.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index 0a840403..a64bb73a 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -1,5 +1,3 @@
-(* 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
is the only constraint on the carrier set. *)
diff --git a/theories/mapset.v b/theories/mapset.v
index 20529a20..1d78d1fe 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -1,5 +1,3 @@
-(* 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
constructed finite sets do so as well. *)
diff --git a/theories/natmap.v b/theories/natmap.v
index 5d356484..35d7355f 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -1,5 +1,3 @@
-(* 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
a list with a proof of canonicity. *)
diff --git a/theories/nmap.v b/theories/nmap.v
index 3b2ad6c7..56b692f9 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -1,5 +1,3 @@
-(* 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]. *)
From stdpp Require Import pmap mapset.
diff --git a/theories/numbers.v b/theories/numbers.v
index 35cc5b26..44d57e3f 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,5 +1,3 @@
-(* 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
notations. *)
diff --git a/theories/option.v b/theories/option.v
index c5a73d55..9ba258be 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -1,5 +1,3 @@
-(* 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. *)
From stdpp Require Export tactics.
diff --git a/theories/orders.v b/theories/orders.v
index db754409..2cd710a5 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -1,5 +1,3 @@
-(* 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 *)
From stdpp Require Export tactics.
diff --git a/theories/pmap.v b/theories/pmap.v
index 088ebcb8..211dce64 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -1,5 +1,3 @@
-(* 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
implementation is based on Xavier Leroy's implementation of radix-2 search
diff --git a/theories/prelude.v b/theories/prelude.v
index 15b8d990..01149561 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -1,5 +1,3 @@
-(* Copyright (c) 2012-2019, Coq-std++ developers. *)
-(* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export
base
tactics
diff --git a/theories/pretty.v b/theories/pretty.v
index 2d8c8635..296cccb2 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -1,5 +1,3 @@
-(* 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.
From Coq Require Import Ascii.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 9c442e6d..af527c74 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -1,5 +1,3 @@
-(* 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.
Set Default Proof Using "Type".
diff --git a/theories/propset.v b/theories/propset.v
index 70e649d9..9e29a4e7 100644
--- a/theories/propset.v
+++ b/theories/propset.v
@@ -1,5 +1,3 @@
-(* 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 sets.
Set Default Proof Using "Type".
diff --git a/theories/relations.v b/theories/relations.v
index c395d91a..30a2f096 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -1,5 +1,3 @@
-(* 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
small step semantics. *)
diff --git a/theories/sets.v b/theories/sets.v
index 6841be61..3ecda91d 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1,5 +1,3 @@
-(* 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 sets. Most
importantly, it implements some tactics to automatically solve goals involving
sets. *)
diff --git a/theories/sorting.v b/theories/sorting.v
index 4cd58672..57936e1e 100644
--- a/theories/sorting.v
+++ b/theories/sorting.v
@@ -1,5 +1,3 @@
-(* 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. *)
From Coq Require Export Sorted.
diff --git a/theories/streams.v b/theories/streams.v
index 92304f40..cd7c4ebe 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,5 +1,3 @@
-(* 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 d8866474..4b601d83 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -1,5 +1,3 @@
-(* 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
search trees (uncompressed Patricia trees) as implemented in the file [pmap]
diff --git a/theories/strings.v b/theories/strings.v
index c96ea2be..f83f075b 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -1,5 +1,3 @@
-(* 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.
From stdpp Require Export list.
diff --git a/theories/tactics.v b/theories/tactics.v
index 5b565c62..00e7f9af 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -1,5 +1,3 @@
-(* 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. *)
From Coq Require Import Omega.
diff --git a/theories/vector.v b/theories/vector.v
index ba0408a1..17f1b8f1 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -1,5 +1,3 @@
-(* 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
renames or changes their notations, so that it becomes more consistent with the
diff --git a/theories/zmap.v b/theories/zmap.v
index d4f015b5..005284f6 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -1,5 +1,3 @@
-(* 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]. *)
From stdpp Require Import pmap mapset.
--
GitLab