docs: add LLVM exceptions to Apache 2.0 licensing

Author: favonia

CONTRIBUTING.markdown

@@ -4,4 +4,4 @@ Thank you for your contribution. Here is some important legal stuff.
 
 By submitting a pull request for this project, unless explicitly stated otherwise, you agree to assign your copyright of the contribution to **The RedPRL Development Team** when it is accepted (merged with or without minor changes). You assert that you have full power to assign the copyright, and that any copyright owned by or shared with a third party has been clearly marked with appropriate copyright notices. If you are employed, please check with your employer about the ownership of your contribution.
 
-This would allow us to, for example, change the license of the codebase to Apache 2.0 or transfer the ownership of the project to someone else *without your further consent*. We demand this assignment so that we do not have to ask *everyone* who has ever contributed for these activities. This requires trust, and if you feel uncomfortable about this assignment, please make an explicit note.
+This would allow us to, for example, change the license of the codebase to a different one (_e.g.,_ [Mozilla Public License (MPL) 2.0](https://www.mozilla.org/en-US/MPL/2.0/FAQ/)) or transfer the ownership of the project to someone else *without your further consent*. We demand this assignment so that we do not have to ask *everyone* who has ever contributed for these activities. This requires trust, and if you feel uncomfortable about this assignment, please make an explicit note.

LICENSE

@@ -199,3 +199,20 @@
    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
    See the License for the specific language governing permissions and
    limitations under the License.
+
+
+--- LLVM Exceptions to the Apache 2.0 License ----
+
+As an exception, if, as a result of your compiling your source code, portions
+of this Software are embedded into an Object form of such source code, you
+may redistribute such embedded portions in such Object form without complying
+with the conditions of Sections 4(a), 4(b) and 4(d) of the License.
+
+In addition, if you combine or link compiled forms of this Software with
+software that is licensed under the GPLv2 ("Combined Software") and if a
+court of competent jurisdiction determines that the patent provision (Section
+3), the indemnity provision (Section 9) or other Section of the License
+conflicts with the conditions of the GPLv2, you may retroactively and
+prospectively choose to deem waived or otherwise exclude such Section(s) of
+the License, but only in their entirety and only with respect to the Combined
+Software.

kado.opam

@@ -6,7 +6,7 @@ Cofibrations in Cartecian cubical type theory as described in the paper 'Syntax
 """
 maintainer: "favonia <favonia@gmail.com>"
 authors: "The RedPRL Development Team"
-license: "Apache-2.0"
+license: "Apache-2.0 WITH LLVM-exception"
 homepage: "https://github.com/RedPRL/kado"
 bug-reports: "https://github.com/RedPRL/kado/issues"
 dev-repo: "git+https://github.com/RedPRL/kado.git"