Merge branch 'robbert/copyright' into 'master'

Remove copyright headers, update LICENCE file.

Closes #54

See merge request iris/stdpp!124

LICENSE

 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.
 

theories/base.v

-(* 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

theories/binders.v

-(* 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

theories/boolset.v

-(* 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".

theories/coGset.v

-(* 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].
 

theories/coPset.v

-(* 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:
 

theories/countable.v

-(* 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".

theories/decidable.v

-(* 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. *)

theories/fin.v

-(* 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

theories/fin_map_dom.v

-(* 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. *)

theories/fin_maps.v

-(* 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

theories/fin_sets.v

-(* 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 . *)

theories/finite.v

-(* 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".
 

theories/functions.v

-(* 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".
 

theories/gmap.v

-(* 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.

theories/gmultiset.v

-(* 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".
 

theories/hashset.v

-(* 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. *)

theories/hlist.v

-(* 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.

theories/infinite.v

-(* 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.
 

theories/lexico.v

-(* 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.