diff --git a/LICENSE b/LICENSE
index 0b9458c293683d7b6b651b0c7ea6e9da42c4a5af..fafc41052df9104ddd419f0fa5bdef2e09d36ce8 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 ce3f75462b222f6655d781f736d49ceba0e3a682..0e6fece31159b8d091f21082cb0d806b604ecc5e 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 3fddac91fd7771fbfa2af936c5e46a062045e8c2..995bbdf875a120daf7a3576ecad250143a8a25f1 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 3bfa3b3d394180c7d9d4ddba5db98f1a87468949..8a0d4c54f1b84b1396d60da9639e5ff5c2b2d150 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 84e93102689ccf6efd64078374ed7662fe2ebedc..6736e7ac9365ce13e961d1e5ffeedd7773479dfd 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 4048edf49e582152575e5359a694d488c2c393be..1aefcbe5ee7ea6992a444aa80d1568f916973987 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 4894b0b12c15bfbda481b2facd513c16ce9021dc..9b5373c4257d65e912594272f728f0169fbb4ba1 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 2345ab9ff62c30c7d33fc542c09f438611f5d38c..34f657ad2e033b58de1a781bed1306889f5a3381 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 905c296df5fa3365525b5e4b464b501ebc6d4d20..ab26009904c28f300f310837027f936fcea33c02 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 5ba8bb788b4ee5ddcd9ba095e5759a7766d3358e..f061ada13833c2e965232e8397eb920d8131a7c9 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 e1c7f17d2989f11be6db6aad980418a5ffefa32c..f87cc30127fd950c803724c106aaa0d7f6633370 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 e71f698a407fa1f5823d7281592f7fe67a80d0eb..b91407f491c8dc309e3281b6b55c9d3cc8dce5f0 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 1364e27454995aaf3a87eb0952ee04114f389665..93292786559530c92e814131e793a05052b0ccb9 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 2c28b1f5e29af40b5ba81d5d5bf1edc70378e26b..868a430b336e13894adca08da2b4b6c598c34159 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 cd1db4489f9821920d7d253a94b86da4ce9776d1..8684a92c0d89c92c733bd96cff5ef70d8383c669 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 aab6bd727bba23195e83e269e3433a4a4eaa233c..634b010a2fa1c7a3e6e051e93bb8fae3cb1987ac 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 e0211a160cb7c71524c2979715c92cf2645be23e..cb1f86aafcdc815557952751f66d9a71c74bece6 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 3f845e9fee45729ade7e5a366ff2a33e3cb66a0f..8f017fdfcd79925e5442efdda34c4b08dad9b198 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 232304f6b55e3db2548bdc23ba19b4119450e174..841e9de2616c6307eff9ab64cc4995bcdab21d59 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 c045e5e9910bcf3be7dc3f56be47a58a466c8812..8710637388a1a931c544517d353c1834b4e0a945 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 eb12c9bcdd212d4577c6d173d0f15858a867d9f0..3e7f3553e17df03b90b787ab40fa4884121075d4 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 c692c8eeab67cea904dd688bcc1ad549709d7276..c443682bac01f2bd0e3ff7160dd5ca0038a4530d 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 0a84040389677827423052d6af3ba52357169660..a64bb73a05a0041b4cdc3a9015cc1debeeb151fb 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 20529a20d0f39d0e2e6c5259b776de7c6f607037..1d78d1fe4528f78abdd221ac904a409295853c61 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 5d356484a3465e17e0c717bccc07c1859138e5e7..35d7355f86ab534a907f06f7952c7282d4a6c2a6 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 3b2ad6c7ba562832b502fbf73ef983f6a1378d05..56b692f953ac21c568c1babc05656443b1c68225 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 35cc5b26f73aa0d7d435d96cffb1e56a499bd223..44d57e3f60e7a7b621e7c727cf6da4b1e43bea3d 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 c5a73d5595094314d983b8d89c9d1b8ebc662caa..9ba258be2e04909b3b8a26f09a8c096b814491bc 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 db754409da8e02111df140a9b28d4d4968fa3285..2cd710a521f902b32aa857d171050b14c37cb56f 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 088ebcb8a4106c468180f69fa966e95dee5090a8..211dce6482113dea710aed1877db65e113cca69f 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 15b8d99042cbedad59dbe4be60b08bc86b2d2d00..011495614325486fc9fd7f3b5a98282fdc13b771 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 2d8c863512e5e9307a8907285e4ae78a33e8c5f1..296cccb22ab543f74fcef44fae7651358da98e41 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 9c442e6dc6f7c4faab6b5e2558f01bc8674dcdd2..af527c74412ecdb4cc1c84f6bcab21f9e191468b 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 70e649d9412a502642223b812203a319e3f0a53e..9e29a4e73c1bca738b095779e7743527bdc58fd2 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 c395d91acaa1f389415710ca058981c60cabc71a..30a2f096e06a1a8d6e403f4f0fa0c3aa7cdf932e 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 6841be618e326a5be7c5d50d2d4096770126ee42..3ecda91da667ad85456175b9391ee31c008a0ec0 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 4cd58672a5804daa23b83c6b941a47731d28eeae..57936e1e03c40d45695fd8b980ce0a482a7d9fb8 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 92304f4045604f8cd6fbea8c299d570e82a1083a..cd7c4ebeca0e87a56fa981ed145edd223cd63548 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 d8866474723d4e765796edaee9390d02f58d6de2..4b601d83b0180181ea9b51ca333acfa37372a247 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 c96ea2be9be68cd954540f9938bda24c6fe37ffe..f83f075b172b0e9483097059351e782e71fa5b48 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 5b565c629710b610bd8e4f3f3884879fd1838d7c..00e7f9af1dcbf3bb9edf902d2b5c490d3a470bdb 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 ba0408a1217a69178bb3ab19b950713519b45cc7..17f1b8f10bfa07f731409dec7aa6c6886b1c24b2 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 d4f015b50be22aeb36788821260434d93bba191c..005284f66e45a8f8211afb9d11161051a6af20db 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.