update license

LICENSE-ARTIFACT

+All files in this development, excluding those in docs/, are distributed
+under the terms of the BSD license, included below.
+
+* The development is based on the Coq development of the Iris project.
+  (https://gitlab.mpi-sws.org/iris/iris)
+  Copyright: Iris developers and contributors
+* The files 
+  - `theories/algebra/ordinals/set_sets.v`, 
+  - `theories/algebra/ordinals/set_ordinals.v`,
+  - `theories/algebra/ordinals/set_functions.v` 
+  are based on the Coq development of
+      "Formalised Set Theory: Well-Orderings and the Axiom of Choice", Dominik Kirst.
+      Available at https://www.ps.uni-saarland.de/~kirst/bachelor.php
+* The file `theories/algebra/ordinals/set_model.v` is based on the Coq development of
+      "Large Model Constructions for Second-Order ZF in Dependent Type Theory"
+        by Dominik Kirst and Gert Smolka, CPP 2018
+        See https://www.ps.uni-saarland.de/Publications/details/KirstSmolka:2017:Large-Model.html. 
+      which in turn is partly based on work by Chad Brown.
+* The files in `theories/examples/safety/barrier/` are adapted from the Iris Examples project.
+  (https://gitlab.mpi-sws.org/iris/examples)
+  Copyright: Iris developers and contributors
+* The file `theories/algebra/auth_frac.v` is taken from the Perennial project https://github.com/mit-pdos/perennial  
+  subject to the MIT license:
+
+      MIT License
+
+      Copyright (c) 2021
+
+      Permission is hereby granted, free of charge, to any person obtaining a copy
+      of this software and associated documentation files (the "Software"), to deal
+      in the Software without restriction, including without limitation the rights
+      to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+      copies of the Software, and to permit persons to whom the Software is
+      furnished to do so, subject to the following conditions:
+
+      The above copyright notice and this permission notice shall be included in
+      all copies or substantial portions of the Software.
+
+      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+      IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+      FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+      AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+      LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+      OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+      THE SOFTWARE. 
+
+* All other files, in particular the files and folders
+  - `theories/program_logic/refinement/`
+  - `theories/base_logic/satisfiable.v`
+  - `theories/bi/satisfiable.v`
+  - `theories/heap_lang/refinement_adequacy.v`
+  - `theories/heap_lang/termination_adequacy.v`
+  - `theories/examples/` except for `theories/examples/safety/`
+  - `theories/algebra/ordinals/arithmetic.v`
+  - `theories/algebra/ordinals/ord_stepindex.v`
+  - `theories/algebra/wf_IR.v`
+  - `theories/algebra/cofe_solver.v`
+are Copyright: Transfinite Iris developers.
+
+
+------------------------------------------------------------------------------
+
+                            BSD LICENCE
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * 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.
+
+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
+(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
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

LICENSE-CODE

 All files in this development, excluding those in docs/, are distributed
 under the terms of the BSD license, included below.
 
+* The development is based on the Coq development of the Iris project.
+  (https://gitlab.mpi-sws.org/iris/iris)
+  Copyright: Iris developers and contributors
+* The files 
+  - `theories/algebra/ordinals/set_sets.v`, 
+  - `theories/algebra/ordinals/set_ordinals.v`,
+  - `theories/algebra/ordinals/set_functions.v` 
+  are based on the Coq development of
+      "Formalised Set Theory: Well-Orderings and the Axiom of Choice", Dominik Kirst.
+      Available at https://www.ps.uni-saarland.de/~kirst/bachelor.php
+* The file `theories/algebra/ordinals/set_model.v` is based on the Coq development of
+      "Large Model Constructions for Second-Order ZF in Dependent Type Theory"
+        by Dominik Kirst and Gert Smolka, CPP 2018
+        See https://www.ps.uni-saarland.de/Publications/details/KirstSmolka:2017:Large-Model.html. 
+      which in turn is partly based on work by Chad Brown.
+* The files in `theories/examples/safety/barrier/` are adapted from the Iris Examples project.
+  (https://gitlab.mpi-sws.org/iris/examples)
+  Copyright: Iris developers and contributors
+* The file `theories/algebra/auth_frac.v` is taken from the Perennial project https://github.com/mit-pdos/perennial  
+  subject to the MIT license:
+
+      MIT License
+
+      Copyright (c) 2021
+
+      Permission is hereby granted, free of charge, to any person obtaining a copy
+      of this software and associated documentation files (the "Software"), to deal
+      in the Software without restriction, including without limitation the rights
+      to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+      copies of the Software, and to permit persons to whom the Software is
+      furnished to do so, subject to the following conditions:
+
+      The above copyright notice and this permission notice shall be included in
+      all copies or substantial portions of the Software.
+
+      THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+      IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+      FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+      AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+      LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+      OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+      THE SOFTWARE. 
+
+* All other files, in particular the files and folders
+  - `theories/program_logic/refinement/`
+  - `theories/base_logic/satisfiable.v`
+  - `theories/bi/satisfiable.v`
+  - `theories/examples/` except for `theories/examples/safety/`
+  - `theories/algebra/ordinals/arithmetic.v`
+  - `theories/algebra/ordinals/ord_stepindex.v`
+  - `theories/algebra/wf_IR.v`
+  - `theories/algebra/cofe_solver.v`
+are Copyright: Transfinite Iris developers.
+
+
 ------------------------------------------------------------------------------
 
                             BSD LICENCE