diff --git a/LICENSE b/LICENSE-APACHE
similarity index 100%
rename from LICENSE
rename to LICENSE-APACHE
diff --git a/LICENSE-MIT b/LICENSE-MIT
new file mode 100644
index 000000000..e694ca1d5
--- /dev/null
+++ b/LICENSE-MIT
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 Eurydice Contributors
+
+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.
diff --git a/README.md b/README.md
index 1ae1e5747..cca80f42c 100644
--- a/README.md
+++ b/README.md
@@ -79,6 +79,6 @@ $ ./krml --help
 
 ## License
 
-KaRaMeL is released under the [Apache 2.0 license]; see `LICENSE` for more details.
+KaRaMeL is released under the [Apache 2.0 license] and MIT license; see `LICENSE-*` for more details.
 
 [Apache 2.0 license]: https://www.apache.org/licenses/LICENSE-2.0
diff --git a/include/krml/c_endianness.h b/include/krml/c_endianness.h
index 21d7e1b4f..937d8d109 100644
--- a/include/krml/c_endianness.h
+++ b/include/krml/c_endianness.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef __KRML_ENDIAN_H
 #define __KRML_ENDIAN_H
diff --git a/include/krml/internal/builtin.h b/include/krml/internal/builtin.h
index 6098f30be..bb47d64d4 100644
--- a/include/krml/internal/builtin.h
+++ b/include/krml/internal/builtin.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef __KRML_BUILTIN_H
 #define __KRML_BUILTIN_H
diff --git a/include/krml/internal/callconv.h b/include/krml/internal/callconv.h
index aeca0ba71..4bc0f878d 100644
--- a/include/krml/internal/callconv.h
+++ b/include/krml/internal/callconv.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef __KRML_CALLCONV_H
 #define __KRML_CALLCONV_H
diff --git a/include/krml/internal/compat.h b/include/krml/internal/compat.h
index b557bbc1b..f206520fc 100644
--- a/include/krml/internal/compat.h
+++ b/include/krml/internal/compat.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef KRML_COMPAT_H
 #define KRML_COMPAT_H
diff --git a/include/krml/internal/debug.h b/include/krml/internal/debug.h
index 786db147e..97f069958 100644
--- a/include/krml/internal/debug.h
+++ b/include/krml/internal/debug.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef __KRML_DEBUG_H
 #define __KRML_DEBUG_H
diff --git a/include/krml/internal/target.h b/include/krml/internal/target.h
index 8e00f2fd2..a13141058 100644
--- a/include/krml/internal/target.h
+++ b/include/krml/internal/target.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef __KRML_TARGET_H
 #define __KRML_TARGET_H
diff --git a/include/krml/internal/types.h b/include/krml/internal/types.h
index e41b39be9..31476313c 100644
--- a/include/krml/internal/types.h
+++ b/include/krml/internal/types.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef KRML_TYPES_H
 #define KRML_TYPES_H
diff --git a/include/krml/internal/wasmsupport.h b/include/krml/internal/wasmsupport.h
index b44fa3f75..5aba97565 100644
--- a/include/krml/internal/wasmsupport.h
+++ b/include/krml/internal/wasmsupport.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /* This file is automatically included when compiling with -wasm -d force-c */
 #define WasmSupport_check_buffer_size(X)
diff --git a/include/krml/lowstar_endianness.h b/include/krml/lowstar_endianness.h
index 1aa2ccd64..af6b882cf 100644
--- a/include/krml/lowstar_endianness.h
+++ b/include/krml/lowstar_endianness.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef __LOWSTAR_ENDIANNESS_H
 #define __LOWSTAR_ENDIANNESS_H
diff --git a/krmllib/c/c.c b/krmllib/c/c.c
index bffc2b9a8..44033dda0 100644
--- a/krmllib/c/c.c
+++ b/krmllib/c/c.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include <stdlib.h>
 #include <stdbool.h>
diff --git a/krmllib/c/c_string.c b/krmllib/c/c_string.c
index e2bb26992..c38ae123d 100644
--- a/krmllib/c/c_string.c
+++ b/krmllib/c/c_string.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "C_String.h"
 
diff --git a/krmllib/c/fstar_bytes.c b/krmllib/c/fstar_bytes.c
index 334bf6dc1..2ef5c826f 100644
--- a/krmllib/c/fstar_bytes.c
+++ b/krmllib/c/fstar_bytes.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /******************************************************************************/
 /* NOT LOW*: implementing FStar.Bytes.bytes as leaky fat pointers with a      */
diff --git a/krmllib/c/fstar_char.c b/krmllib/c/fstar_char.c
index f6931522e..0ac2042f7 100644
--- a/krmllib/c/fstar_char.c
+++ b/krmllib/c/fstar_char.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Char.h"
 
diff --git a/krmllib/c/fstar_date.c b/krmllib/c/fstar_date.c
index d5185866e..c29e7c5e1 100644
--- a/krmllib/c/fstar_date.c
+++ b/krmllib/c/fstar_date.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Date.h"
 
diff --git a/krmllib/c/fstar_dyn.c b/krmllib/c/fstar_dyn.c
index 521cb6104..ad4fef60c 100644
--- a/krmllib/c/fstar_dyn.c
+++ b/krmllib/c/fstar_dyn.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include <krml/internal/types.h>
 
diff --git a/krmllib/c/fstar_hyperstack_io.c b/krmllib/c/fstar_hyperstack_io.c
index 8b2f7e652..9980bb573 100644
--- a/krmllib/c/fstar_hyperstack_io.c
+++ b/krmllib/c/fstar_hyperstack_io.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_HyperStack_IO.h"
 
diff --git a/krmllib/c/fstar_int16.c b/krmllib/c/fstar_int16.c
index 5339be588..f8f9fdbd3 100644
--- a/krmllib/c/fstar_int16.c
+++ b/krmllib/c/fstar_int16.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int16.h"
 
diff --git a/krmllib/c/fstar_int32.c b/krmllib/c/fstar_int32.c
index 370ed2609..cbf9dcd53 100644
--- a/krmllib/c/fstar_int32.c
+++ b/krmllib/c/fstar_int32.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int32.h"
 
diff --git a/krmllib/c/fstar_int64.c b/krmllib/c/fstar_int64.c
index 0f481c613..5f6108906 100644
--- a/krmllib/c/fstar_int64.c
+++ b/krmllib/c/fstar_int64.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int64.h"
 
diff --git a/krmllib/c/fstar_int8.c b/krmllib/c/fstar_int8.c
index 25f4609e2..0de549aff 100644
--- a/krmllib/c/fstar_int8.c
+++ b/krmllib/c/fstar_int8.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int8.h"
 
diff --git a/krmllib/c/fstar_io.c b/krmllib/c/fstar_io.c
index ab4b64a70..6eaabdc23 100644
--- a/krmllib/c/fstar_io.c
+++ b/krmllib/c/fstar_io.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_IO.h"
 
diff --git a/krmllib/c/fstar_string.c b/krmllib/c/fstar_string.c
index 1117bfa29..6539508b8 100644
--- a/krmllib/c/fstar_string.c
+++ b/krmllib/c/fstar_string.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "Prims.h"
 #include "FStar_String.h"
diff --git a/krmllib/c/fstar_uint128_gcc64.h b/krmllib/c/fstar_uint128_gcc64.h
index ae109004f..10a4dc1aa 100644
--- a/krmllib/c/fstar_uint128_gcc64.h
+++ b/krmllib/c/fstar_uint128_gcc64.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /******************************************************************************/
 /* Machine integers (128-bit arithmetic)                                      */
diff --git a/krmllib/c/fstar_uint128_msvc.h b/krmllib/c/fstar_uint128_msvc.h
index 6ff658f54..89bbc1593 100644
--- a/krmllib/c/fstar_uint128_msvc.h
+++ b/krmllib/c/fstar_uint128_msvc.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /* This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  * then hand-edited to use MSVC intrinsics KaRaMeL invocation:
diff --git a/krmllib/c/fstar_uint128_struct_endianness.h b/krmllib/c/fstar_uint128_struct_endianness.h
index e2b6d6285..bb736add3 100644
--- a/krmllib/c/fstar_uint128_struct_endianness.h
+++ b/krmllib/c/fstar_uint128_struct_endianness.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H
 #define FSTAR_UINT128_STRUCT_ENDIANNESS_H
diff --git a/krmllib/c/fstar_uint16.c b/krmllib/c/fstar_uint16.c
index c5083da5b..2df589a48 100644
--- a/krmllib/c/fstar_uint16.c
+++ b/krmllib/c/fstar_uint16.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/c/fstar_uint32.c b/krmllib/c/fstar_uint32.c
index 9b75676ac..69903df74 100644
--- a/krmllib/c/fstar_uint32.c
+++ b/krmllib/c/fstar_uint32.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/c/fstar_uint64.c b/krmllib/c/fstar_uint64.c
index 56e1eb709..55a0c0532 100644
--- a/krmllib/c/fstar_uint64.c
+++ b/krmllib/c/fstar_uint64.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/c/fstar_uint8.c b/krmllib/c/fstar_uint8.c
index 564668499..31caa5fbc 100644
--- a/krmllib/c/fstar_uint8.c
+++ b/krmllib/c/fstar_uint8.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/c/prims.c b/krmllib/c/prims.c
index eebeb1f1b..ba08cb069 100644
--- a/krmllib/c/prims.c
+++ b/krmllib/c/prims.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "Prims.h"
 #include "FStar_Int32.h"
diff --git a/krmllib/c/testlib.c b/krmllib/c/testlib.c
index cbbfdbe71..54605379d 100644
--- a/krmllib/c/testlib.c
+++ b/krmllib/c/testlib.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "TestLib.h"
 
diff --git a/krmllib/copyright-header.txt b/krmllib/copyright-header.txt
index 059004351..f51cbf21f 100644
--- a/krmllib/copyright-header.txt
+++ b/krmllib/copyright-header.txt
@@ -1,4 +1,4 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
diff --git a/krmllib/dist/generic/C.h b/krmllib/dist/generic/C.h
index 007a98ea1..8ba1a91d3 100644
--- a/krmllib/dist/generic/C.h
+++ b/krmllib/dist/generic/C.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/C_Failure.h b/krmllib/dist/generic/C_Failure.h
index 0efca553d..3955f3038 100644
--- a/krmllib/dist/generic/C_Failure.h
+++ b/krmllib/dist/generic/C_Failure.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/C_Loops.h b/krmllib/dist/generic/C_Loops.h
index 39efd5f1f..cc5fb340b 100644
--- a/krmllib/dist/generic/C_Loops.h
+++ b/krmllib/dist/generic/C_Loops.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/C_String.h b/krmllib/dist/generic/C_String.h
index 62a135ce9..4ad0caf23 100644
--- a/krmllib/dist/generic/C_String.h
+++ b/krmllib/dist/generic/C_String.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_All.h b/krmllib/dist/generic/FStar_All.h
index fce00b0ca..68a8fe76a 100644
--- a/krmllib/dist/generic/FStar_All.h
+++ b/krmllib/dist/generic/FStar_All.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_BigOps.h b/krmllib/dist/generic/FStar_BigOps.h
index 4a5be33df..937b721ad 100644
--- a/krmllib/dist/generic/FStar_BigOps.h
+++ b/krmllib/dist/generic/FStar_BigOps.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_BitVector.h b/krmllib/dist/generic/FStar_BitVector.h
index 4fd279f27..7b4bcff33 100644
--- a/krmllib/dist/generic/FStar_BitVector.h
+++ b/krmllib/dist/generic/FStar_BitVector.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Bytes.h b/krmllib/dist/generic/FStar_Bytes.h
index e18f74fb0..2f478715b 100644
--- a/krmllib/dist/generic/FStar_Bytes.h
+++ b/krmllib/dist/generic/FStar_Bytes.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Calc.h b/krmllib/dist/generic/FStar_Calc.h
index 9e94b04bb..4c03ecbd0 100644
--- a/krmllib/dist/generic/FStar_Calc.h
+++ b/krmllib/dist/generic/FStar_Calc.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Char.h b/krmllib/dist/generic/FStar_Char.h
index da2fbc3ad..baeeda657 100644
--- a/krmllib/dist/generic/FStar_Char.h
+++ b/krmllib/dist/generic/FStar_Char.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Date.h b/krmllib/dist/generic/FStar_Date.h
index b89a459ca..1be0a5827 100644
--- a/krmllib/dist/generic/FStar_Date.h
+++ b/krmllib/dist/generic/FStar_Date.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_ErasedLogic.h b/krmllib/dist/generic/FStar_ErasedLogic.h
index 76786ea0e..be0158f73 100644
--- a/krmllib/dist/generic/FStar_ErasedLogic.h
+++ b/krmllib/dist/generic/FStar_ErasedLogic.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Float.h b/krmllib/dist/generic/FStar_Float.h
index 5061a5ee2..09925195d 100644
--- a/krmllib/dist/generic/FStar_Float.h
+++ b/krmllib/dist/generic/FStar_Float.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_FunctionalExtensionality.h b/krmllib/dist/generic/FStar_FunctionalExtensionality.h
index d1904eb14..b45f98066 100644
--- a/krmllib/dist/generic/FStar_FunctionalExtensionality.h
+++ b/krmllib/dist/generic/FStar_FunctionalExtensionality.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_GSet.h b/krmllib/dist/generic/FStar_GSet.h
index 0d81e6d0e..83c2434cd 100644
--- a/krmllib/dist/generic/FStar_GSet.h
+++ b/krmllib/dist/generic/FStar_GSet.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Heap.h b/krmllib/dist/generic/FStar_Heap.h
index 66e40ce5a..c9baea598 100644
--- a/krmllib/dist/generic/FStar_Heap.h
+++ b/krmllib/dist/generic/FStar_Heap.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_HyperStack_All.h b/krmllib/dist/generic/FStar_HyperStack_All.h
index e0d2df86c..f94067aca 100644
--- a/krmllib/dist/generic/FStar_HyperStack_All.h
+++ b/krmllib/dist/generic/FStar_HyperStack_All.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_HyperStack_IO.h b/krmllib/dist/generic/FStar_HyperStack_IO.h
index 68aff4043..d5ce93dda 100644
--- a/krmllib/dist/generic/FStar_HyperStack_IO.h
+++ b/krmllib/dist/generic/FStar_HyperStack_IO.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_HyperStack_ST.h b/krmllib/dist/generic/FStar_HyperStack_ST.h
index 7074a7c67..74e59bb1e 100644
--- a/krmllib/dist/generic/FStar_HyperStack_ST.h
+++ b/krmllib/dist/generic/FStar_HyperStack_ST.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_IO.h b/krmllib/dist/generic/FStar_IO.h
index b12573871..f01730b3d 100644
--- a/krmllib/dist/generic/FStar_IO.h
+++ b/krmllib/dist/generic/FStar_IO.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Int.h b/krmllib/dist/generic/FStar_Int.h
index 055223afd..9d0c4b52f 100644
--- a/krmllib/dist/generic/FStar_Int.h
+++ b/krmllib/dist/generic/FStar_Int.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Int16.h b/krmllib/dist/generic/FStar_Int16.h
index c2c6c2a05..d15d1aff8 100644
--- a/krmllib/dist/generic/FStar_Int16.h
+++ b/krmllib/dist/generic/FStar_Int16.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Int32.h b/krmllib/dist/generic/FStar_Int32.h
index a43806a1a..cd88b59dd 100644
--- a/krmllib/dist/generic/FStar_Int32.h
+++ b/krmllib/dist/generic/FStar_Int32.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Int64.h b/krmllib/dist/generic/FStar_Int64.h
index d39eba340..7c8020834 100644
--- a/krmllib/dist/generic/FStar_Int64.h
+++ b/krmllib/dist/generic/FStar_Int64.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Int8.h b/krmllib/dist/generic/FStar_Int8.h
index e8539aa1c..8e83d365a 100644
--- a/krmllib/dist/generic/FStar_Int8.h
+++ b/krmllib/dist/generic/FStar_Int8.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Int_Cast.h b/krmllib/dist/generic/FStar_Int_Cast.h
index d71788bac..b287c1fb0 100644
--- a/krmllib/dist/generic/FStar_Int_Cast.h
+++ b/krmllib/dist/generic/FStar_Int_Cast.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Issue.h b/krmllib/dist/generic/FStar_Issue.h
index ed9e61b9d..c0e1bf70d 100644
--- a/krmllib/dist/generic/FStar_Issue.h
+++ b/krmllib/dist/generic/FStar_Issue.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Krml_Endianness.h b/krmllib/dist/generic/FStar_Krml_Endianness.h
index 6cca90e76..50d2e560a 100644
--- a/krmllib/dist/generic/FStar_Krml_Endianness.h
+++ b/krmllib/dist/generic/FStar_Krml_Endianness.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_List_Tot_Base.h b/krmllib/dist/generic/FStar_List_Tot_Base.h
index 34d242ba5..ed036a032 100644
--- a/krmllib/dist/generic/FStar_List_Tot_Base.h
+++ b/krmllib/dist/generic/FStar_List_Tot_Base.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_List_Tot_Properties.h b/krmllib/dist/generic/FStar_List_Tot_Properties.h
index 6b9f99837..78efd8c06 100644
--- a/krmllib/dist/generic/FStar_List_Tot_Properties.h
+++ b/krmllib/dist/generic/FStar_List_Tot_Properties.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Map.h b/krmllib/dist/generic/FStar_Map.h
index 0f0d92b59..cbd0a04f7 100644
--- a/krmllib/dist/generic/FStar_Map.h
+++ b/krmllib/dist/generic/FStar_Map.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Math_Lib.h b/krmllib/dist/generic/FStar_Math_Lib.h
index cc9957372..566361980 100644
--- a/krmllib/dist/generic/FStar_Math_Lib.h
+++ b/krmllib/dist/generic/FStar_Math_Lib.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_ModifiesGen.c b/krmllib/dist/generic/FStar_ModifiesGen.c
index 4073495ea..794a685b5 100644
--- a/krmllib/dist/generic/FStar_ModifiesGen.c
+++ b/krmllib/dist/generic/FStar_ModifiesGen.c
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_ModifiesGen.h b/krmllib/dist/generic/FStar_ModifiesGen.h
index dbd364802..532cfdd2c 100644
--- a/krmllib/dist/generic/FStar_ModifiesGen.h
+++ b/krmllib/dist/generic/FStar_ModifiesGen.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Monotonic_Heap.h b/krmllib/dist/generic/FStar_Monotonic_Heap.h
index 5a117951f..c38b4d9eb 100644
--- a/krmllib/dist/generic/FStar_Monotonic_Heap.h
+++ b/krmllib/dist/generic/FStar_Monotonic_Heap.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Monotonic_HyperHeap.h b/krmllib/dist/generic/FStar_Monotonic_HyperHeap.h
index d652f02e2..ea8dd484a 100644
--- a/krmllib/dist/generic/FStar_Monotonic_HyperHeap.h
+++ b/krmllib/dist/generic/FStar_Monotonic_HyperHeap.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Monotonic_HyperStack.h b/krmllib/dist/generic/FStar_Monotonic_HyperStack.h
index 158e3073d..22f86f3bb 100644
--- a/krmllib/dist/generic/FStar_Monotonic_HyperStack.h
+++ b/krmllib/dist/generic/FStar_Monotonic_HyperStack.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Monotonic_Pure.h b/krmllib/dist/generic/FStar_Monotonic_Pure.h
index 58d18d86e..2420bf7cd 100644
--- a/krmllib/dist/generic/FStar_Monotonic_Pure.h
+++ b/krmllib/dist/generic/FStar_Monotonic_Pure.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Mul.h b/krmllib/dist/generic/FStar_Mul.h
index e813cf91f..7008c3554 100644
--- a/krmllib/dist/generic/FStar_Mul.h
+++ b/krmllib/dist/generic/FStar_Mul.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Order.c b/krmllib/dist/generic/FStar_Order.c
index 65714c9fd..45d4fe3e1 100644
--- a/krmllib/dist/generic/FStar_Order.c
+++ b/krmllib/dist/generic/FStar_Order.c
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Order.h b/krmllib/dist/generic/FStar_Order.h
index 62e633cc1..397f44ee8 100644
--- a/krmllib/dist/generic/FStar_Order.h
+++ b/krmllib/dist/generic/FStar_Order.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Pervasives.h b/krmllib/dist/generic/FStar_Pervasives.h
index bbf617696..f852a7a60 100644
--- a/krmllib/dist/generic/FStar_Pervasives.h
+++ b/krmllib/dist/generic/FStar_Pervasives.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_PredicateExtensionality.h b/krmllib/dist/generic/FStar_PredicateExtensionality.h
index 7c5365854..db10934c2 100644
--- a/krmllib/dist/generic/FStar_PredicateExtensionality.h
+++ b/krmllib/dist/generic/FStar_PredicateExtensionality.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Preorder.h b/krmllib/dist/generic/FStar_Preorder.h
index a1a0e2c72..8e694b8bc 100644
--- a/krmllib/dist/generic/FStar_Preorder.h
+++ b/krmllib/dist/generic/FStar_Preorder.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_ST.h b/krmllib/dist/generic/FStar_ST.h
index dcde5b155..baf9b9fac 100644
--- a/krmllib/dist/generic/FStar_ST.h
+++ b/krmllib/dist/generic/FStar_ST.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Sealed_Inhabited.h b/krmllib/dist/generic/FStar_Sealed_Inhabited.h
index 3c91f00b8..6f650baa2 100644
--- a/krmllib/dist/generic/FStar_Sealed_Inhabited.h
+++ b/krmllib/dist/generic/FStar_Sealed_Inhabited.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Seq_Base.h b/krmllib/dist/generic/FStar_Seq_Base.h
index 32f80cc9c..8ffd92847 100644
--- a/krmllib/dist/generic/FStar_Seq_Base.h
+++ b/krmllib/dist/generic/FStar_Seq_Base.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Seq_Properties.h b/krmllib/dist/generic/FStar_Seq_Properties.h
index 5cb4718f7..de461b1a9 100644
--- a/krmllib/dist/generic/FStar_Seq_Properties.h
+++ b/krmllib/dist/generic/FStar_Seq_Properties.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_Set.h b/krmllib/dist/generic/FStar_Set.h
index bf7039bb2..557c619a5 100644
--- a/krmllib/dist/generic/FStar_Set.h
+++ b/krmllib/dist/generic/FStar_Set.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_String.h b/krmllib/dist/generic/FStar_String.h
index 929ce6666..51a19f845 100644
--- a/krmllib/dist/generic/FStar_String.h
+++ b/krmllib/dist/generic/FStar_String.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_TSet.h b/krmllib/dist/generic/FStar_TSet.h
index 2fbbf84ba..1511990fa 100644
--- a/krmllib/dist/generic/FStar_TSet.h
+++ b/krmllib/dist/generic/FStar_TSet.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_UInt.h b/krmllib/dist/generic/FStar_UInt.h
index af8e54111..7d73cddb5 100644
--- a/krmllib/dist/generic/FStar_UInt.h
+++ b/krmllib/dist/generic/FStar_UInt.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_UInt128.h b/krmllib/dist/generic/FStar_UInt128.h
index 6cfb81b53..710ce36de 100644
--- a/krmllib/dist/generic/FStar_UInt128.h
+++ b/krmllib/dist/generic/FStar_UInt128.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_UInt128_Verified.h b/krmllib/dist/generic/FStar_UInt128_Verified.h
index 9e4e2290b..d4a90220b 100644
--- a/krmllib/dist/generic/FStar_UInt128_Verified.h
+++ b/krmllib/dist/generic/FStar_UInt128_Verified.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_UInt_8_16_32_64.h b/krmllib/dist/generic/FStar_UInt_8_16_32_64.h
index 78d7cc62f..57bfdafcc 100644
--- a/krmllib/dist/generic/FStar_UInt_8_16_32_64.h
+++ b/krmllib/dist/generic/FStar_UInt_8_16_32_64.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/FStar_VConfig.h b/krmllib/dist/generic/FStar_VConfig.h
index ba5e170f6..1501dad44 100644
--- a/krmllib/dist/generic/FStar_VConfig.h
+++ b/krmllib/dist/generic/FStar_VConfig.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/LowStar_Endianness.h b/krmllib/dist/generic/LowStar_Endianness.h
index 6a416677a..1a3b5cfac 100644
--- a/krmllib/dist/generic/LowStar_Endianness.h
+++ b/krmllib/dist/generic/LowStar_Endianness.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/LowStar_Monotonic_Buffer.h b/krmllib/dist/generic/LowStar_Monotonic_Buffer.h
index 7e77ae3fd..4139940c2 100644
--- a/krmllib/dist/generic/LowStar_Monotonic_Buffer.h
+++ b/krmllib/dist/generic/LowStar_Monotonic_Buffer.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/LowStar_Printf.h b/krmllib/dist/generic/LowStar_Printf.h
index c3d552b5c..82ed7bc33 100644
--- a/krmllib/dist/generic/LowStar_Printf.h
+++ b/krmllib/dist/generic/LowStar_Printf.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/Prims.h b/krmllib/dist/generic/Prims.h
index 6170261ae..e9688c05e 100644
--- a/krmllib/dist/generic/Prims.h
+++ b/krmllib/dist/generic/Prims.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/TestLib.h b/krmllib/dist/generic/TestLib.h
index b1f0c6bb7..55b0556f6 100644
--- a/krmllib/dist/generic/TestLib.h
+++ b/krmllib/dist/generic/TestLib.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/WasmSupport.c b/krmllib/dist/generic/WasmSupport.c
index 507785f51..44d266186 100644
--- a/krmllib/dist/generic/WasmSupport.c
+++ b/krmllib/dist/generic/WasmSupport.c
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/WasmSupport.h b/krmllib/dist/generic/WasmSupport.h
index e92b2665f..b8dbf60a1 100644
--- a/krmllib/dist/generic/WasmSupport.h
+++ b/krmllib/dist/generic/WasmSupport.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/generic/c.c b/krmllib/dist/generic/c.c
index bffc2b9a8..44033dda0 100644
--- a/krmllib/dist/generic/c.c
+++ b/krmllib/dist/generic/c.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include <stdlib.h>
 #include <stdbool.h>
diff --git a/krmllib/dist/generic/c_string.c b/krmllib/dist/generic/c_string.c
index e2bb26992..c38ae123d 100644
--- a/krmllib/dist/generic/c_string.c
+++ b/krmllib/dist/generic/c_string.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "C_String.h"
 
diff --git a/krmllib/dist/generic/fstar_bytes.c b/krmllib/dist/generic/fstar_bytes.c
index 334bf6dc1..2ef5c826f 100644
--- a/krmllib/dist/generic/fstar_bytes.c
+++ b/krmllib/dist/generic/fstar_bytes.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /******************************************************************************/
 /* NOT LOW*: implementing FStar.Bytes.bytes as leaky fat pointers with a      */
diff --git a/krmllib/dist/generic/fstar_char.c b/krmllib/dist/generic/fstar_char.c
index f6931522e..0ac2042f7 100644
--- a/krmllib/dist/generic/fstar_char.c
+++ b/krmllib/dist/generic/fstar_char.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Char.h"
 
diff --git a/krmllib/dist/generic/fstar_date.c b/krmllib/dist/generic/fstar_date.c
index d5185866e..c29e7c5e1 100644
--- a/krmllib/dist/generic/fstar_date.c
+++ b/krmllib/dist/generic/fstar_date.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Date.h"
 
diff --git a/krmllib/dist/generic/fstar_dyn.c b/krmllib/dist/generic/fstar_dyn.c
index 521cb6104..ad4fef60c 100644
--- a/krmllib/dist/generic/fstar_dyn.c
+++ b/krmllib/dist/generic/fstar_dyn.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include <krml/internal/types.h>
 
diff --git a/krmllib/dist/generic/fstar_hyperstack_io.c b/krmllib/dist/generic/fstar_hyperstack_io.c
index 8b2f7e652..9980bb573 100644
--- a/krmllib/dist/generic/fstar_hyperstack_io.c
+++ b/krmllib/dist/generic/fstar_hyperstack_io.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_HyperStack_IO.h"
 
diff --git a/krmllib/dist/generic/fstar_int16.c b/krmllib/dist/generic/fstar_int16.c
index 5339be588..f8f9fdbd3 100644
--- a/krmllib/dist/generic/fstar_int16.c
+++ b/krmllib/dist/generic/fstar_int16.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int16.h"
 
diff --git a/krmllib/dist/generic/fstar_int32.c b/krmllib/dist/generic/fstar_int32.c
index 370ed2609..cbf9dcd53 100644
--- a/krmllib/dist/generic/fstar_int32.c
+++ b/krmllib/dist/generic/fstar_int32.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int32.h"
 
diff --git a/krmllib/dist/generic/fstar_int64.c b/krmllib/dist/generic/fstar_int64.c
index 0f481c613..5f6108906 100644
--- a/krmllib/dist/generic/fstar_int64.c
+++ b/krmllib/dist/generic/fstar_int64.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int64.h"
 
diff --git a/krmllib/dist/generic/fstar_int8.c b/krmllib/dist/generic/fstar_int8.c
index 25f4609e2..0de549aff 100644
--- a/krmllib/dist/generic/fstar_int8.c
+++ b/krmllib/dist/generic/fstar_int8.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_Int8.h"
 
diff --git a/krmllib/dist/generic/fstar_io.c b/krmllib/dist/generic/fstar_io.c
index ab4b64a70..6eaabdc23 100644
--- a/krmllib/dist/generic/fstar_io.c
+++ b/krmllib/dist/generic/fstar_io.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_IO.h"
 
diff --git a/krmllib/dist/generic/fstar_string.c b/krmllib/dist/generic/fstar_string.c
index 1117bfa29..6539508b8 100644
--- a/krmllib/dist/generic/fstar_string.c
+++ b/krmllib/dist/generic/fstar_string.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "Prims.h"
 #include "FStar_String.h"
diff --git a/krmllib/dist/generic/fstar_uint128_gcc64.h b/krmllib/dist/generic/fstar_uint128_gcc64.h
index ae109004f..10a4dc1aa 100644
--- a/krmllib/dist/generic/fstar_uint128_gcc64.h
+++ b/krmllib/dist/generic/fstar_uint128_gcc64.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /******************************************************************************/
 /* Machine integers (128-bit arithmetic)                                      */
diff --git a/krmllib/dist/generic/fstar_uint128_msvc.h b/krmllib/dist/generic/fstar_uint128_msvc.h
index 6ff658f54..89bbc1593 100644
--- a/krmllib/dist/generic/fstar_uint128_msvc.h
+++ b/krmllib/dist/generic/fstar_uint128_msvc.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /* This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  * then hand-edited to use MSVC intrinsics KaRaMeL invocation:
diff --git a/krmllib/dist/generic/fstar_uint128_struct_endianness.h b/krmllib/dist/generic/fstar_uint128_struct_endianness.h
index e2b6d6285..bb736add3 100644
--- a/krmllib/dist/generic/fstar_uint128_struct_endianness.h
+++ b/krmllib/dist/generic/fstar_uint128_struct_endianness.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H
 #define FSTAR_UINT128_STRUCT_ENDIANNESS_H
diff --git a/krmllib/dist/generic/fstar_uint16.c b/krmllib/dist/generic/fstar_uint16.c
index c5083da5b..2df589a48 100644
--- a/krmllib/dist/generic/fstar_uint16.c
+++ b/krmllib/dist/generic/fstar_uint16.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/dist/generic/fstar_uint32.c b/krmllib/dist/generic/fstar_uint32.c
index 9b75676ac..69903df74 100644
--- a/krmllib/dist/generic/fstar_uint32.c
+++ b/krmllib/dist/generic/fstar_uint32.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/dist/generic/fstar_uint64.c b/krmllib/dist/generic/fstar_uint64.c
index 56e1eb709..55a0c0532 100644
--- a/krmllib/dist/generic/fstar_uint64.c
+++ b/krmllib/dist/generic/fstar_uint64.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/dist/generic/fstar_uint8.c b/krmllib/dist/generic/fstar_uint8.c
index 564668499..31caa5fbc 100644
--- a/krmllib/dist/generic/fstar_uint8.c
+++ b/krmllib/dist/generic/fstar_uint8.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "FStar_UInt_8_16_32_64.h"
 
diff --git a/krmllib/dist/generic/prims.c b/krmllib/dist/generic/prims.c
index eebeb1f1b..ba08cb069 100644
--- a/krmllib/dist/generic/prims.c
+++ b/krmllib/dist/generic/prims.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "Prims.h"
 #include "FStar_Int32.h"
diff --git a/krmllib/dist/generic/testlib.c b/krmllib/dist/generic/testlib.c
index cbbfdbe71..54605379d 100644
--- a/krmllib/dist/generic/testlib.c
+++ b/krmllib/dist/generic/testlib.c
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #include "TestLib.h"
 
diff --git a/krmllib/dist/minimal/FStar_UInt128.h b/krmllib/dist/minimal/FStar_UInt128.h
index ecc90213c..be32ad9b6 100644
--- a/krmllib/dist/minimal/FStar_UInt128.h
+++ b/krmllib/dist/minimal/FStar_UInt128.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/minimal/FStar_UInt128_Verified.h b/krmllib/dist/minimal/FStar_UInt128_Verified.h
index 9e4e2290b..d4a90220b 100644
--- a/krmllib/dist/minimal/FStar_UInt128_Verified.h
+++ b/krmllib/dist/minimal/FStar_UInt128_Verified.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h b/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
index 56a2454fc..39ac471f3 100644
--- a/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
+++ b/krmllib/dist/minimal/FStar_UInt_8_16_32_64.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/minimal/LowStar_Endianness.h b/krmllib/dist/minimal/LowStar_Endianness.h
index e851c15c9..f95743d4d 100644
--- a/krmllib/dist/minimal/LowStar_Endianness.h
+++ b/krmllib/dist/minimal/LowStar_Endianness.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/minimal/fstar_uint128_gcc64.h b/krmllib/dist/minimal/fstar_uint128_gcc64.h
index ae109004f..10a4dc1aa 100644
--- a/krmllib/dist/minimal/fstar_uint128_gcc64.h
+++ b/krmllib/dist/minimal/fstar_uint128_gcc64.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /******************************************************************************/
 /* Machine integers (128-bit arithmetic)                                      */
diff --git a/krmllib/dist/minimal/fstar_uint128_msvc.h b/krmllib/dist/minimal/fstar_uint128_msvc.h
index 6ff658f54..89bbc1593 100644
--- a/krmllib/dist/minimal/fstar_uint128_msvc.h
+++ b/krmllib/dist/minimal/fstar_uint128_msvc.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 /* This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  * then hand-edited to use MSVC intrinsics KaRaMeL invocation:
diff --git a/krmllib/dist/minimal/fstar_uint128_struct_endianness.h b/krmllib/dist/minimal/fstar_uint128_struct_endianness.h
index e2b6d6285..bb736add3 100644
--- a/krmllib/dist/minimal/fstar_uint128_struct_endianness.h
+++ b/krmllib/dist/minimal/fstar_uint128_struct_endianness.h
@@ -1,5 +1,5 @@
 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-   Licensed under the Apache 2.0 License. */
+   Licensed under the Apache 2.0 and MIT Licenses. */
 
 #ifndef FSTAR_UINT128_STRUCT_ENDIANNESS_H
 #define FSTAR_UINT128_STRUCT_ENDIANNESS_H
diff --git a/krmllib/dist/uint128/FStar_UInt128_Verified.h b/krmllib/dist/uint128/FStar_UInt128_Verified.h
index 9e4e2290b..d4a90220b 100644
--- a/krmllib/dist/uint128/FStar_UInt128_Verified.h
+++ b/krmllib/dist/uint128/FStar_UInt128_Verified.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/krmllib/dist/uint128/FStar_UInt_8_16_32_64.h b/krmllib/dist/uint128/FStar_UInt_8_16_32_64.h
index aa53cf8a9..3fea56bc6 100644
--- a/krmllib/dist/uint128/FStar_UInt_8_16_32_64.h
+++ b/krmllib/dist/uint128/FStar_UInt_8_16_32_64.h
@@ -1,6 +1,6 @@
 /*
   Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
-  Licensed under the Apache 2.0 License.
+  Licensed under the Apache 2.0 and MIT Licenses.
 */
 
 
diff --git a/lib/Ast.ml b/lib/Ast.ml
index fa1d366bd..50cd666d4 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** The internal, typed AST that we perform all transformations on. *)
 
diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml
index bcfa32f7b..4e39a64c2 100644
--- a/lib/AstToCFlat.ml
+++ b/lib/AstToCFlat.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Going from CStar to CFlat *)
 
diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml
index 7d443148a..49d80a623 100644
--- a/lib/AstToCStar.ml
+++ b/lib/AstToCStar.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Translation from Low* to C* *)
 
diff --git a/lib/Atom.ml b/lib/Atom.ml
index 38b103ca5..eef47c8a7 100644
--- a/lib/Atom.ml
+++ b/lib/Atom.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 type t = int
   [@@deriving yojson, show]
diff --git a/lib/Builtin.ml b/lib/Builtin.ml
index cfab084d1..e7446d0ab 100644
--- a/lib/Builtin.ml
+++ b/lib/Builtin.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Removing all traces of F* models and replacing them with built-in
  * definitions or abstract ones before re-checking the program as Low*. *)
diff --git a/lib/Bundle.ml b/lib/Bundle.ml
index 26dda31f6..483d40068 100644
--- a/lib/Bundle.ml
+++ b/lib/Bundle.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** The type of a single bundle -- this avoids a cyclic dependency between
  * [Parser] and [Bundles] *)
diff --git a/lib/Bundles.ml b/lib/Bundles.ml
index 8db31dd9f..eae774af7 100644
--- a/lib/Bundles.ml
+++ b/lib/Bundles.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Collapsing several F* modules into a single "bundle" to allow more static
  * uses. *)
diff --git a/lib/C11.ml b/lib/C11.ml
index 5a3f27f7c..f0515da72 100644
--- a/lib/C11.ml
+++ b/lib/C11.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 module K = Constant
 open Common
diff --git a/lib/CFlat.ml b/lib/CFlat.ml
index bb8ec4fec..1169e3e43 100644
--- a/lib/CFlat.ml
+++ b/lib/CFlat.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** CFlat, without structures and with computed stack frames. *)
 
diff --git a/lib/CFlatToWasm.ml b/lib/CFlatToWasm.ml
index 49f12ba44..ed1107153 100644
--- a/lib/CFlatToWasm.ml
+++ b/lib/CFlatToWasm.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 open CFlat
 open CFlat.Sizes
diff --git a/lib/CStar.ml b/lib/CStar.ml
index fd39c0f7c..657cf294a 100644
--- a/lib/CStar.ml
+++ b/lib/CStar.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Definition of C* *)
 
diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml
index 67c116daa..d0be22a44 100644
--- a/lib/CStarToC11.ml
+++ b/lib/CStarToC11.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Converting from C* to C abstract syntax. *)
 
diff --git a/lib/Checker.ml b/lib/Checker.ml
index 3cbf6c30b..dabb3ce5f 100644
--- a/lib/Checker.ml
+++ b/lib/Checker.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Checking the well-formedness of a program in [Ast] *)
 
diff --git a/lib/Common.ml b/lib/Common.ml
index d5d75fd8f..bb311eefd 100644
--- a/lib/Common.ml
+++ b/lib/Common.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 type calling_convention =
   | StdCall
diff --git a/lib/Constant.ml b/lib/Constant.ml
index 9f80379cb..20de6f99c 100644
--- a/lib/Constant.ml
+++ b/lib/Constant.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Machine integers. Don't repeat the same thing everywhere. *)
 
diff --git a/lib/DataTypes.ml b/lib/DataTypes.ml
index a5336b982..a2499bc1e 100644
--- a/lib/DataTypes.ml
+++ b/lib/DataTypes.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Monormophization of data types, including tuples, then compilation of
  * pattern matches and of data types into structs & unions. *)
diff --git a/lib/DeBruijn.ml b/lib/DeBruijn.ml
index 382c3220d..0ee148085 100644
--- a/lib/DeBruijn.ml
+++ b/lib/DeBruijn.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** This module provides various substitution functions. *)
 
diff --git a/lib/Diagnostics.ml b/lib/Diagnostics.ml
index 7f88fdfa6..bc6fcb3fe 100644
--- a/lib/Diagnostics.ml
+++ b/lib/Diagnostics.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Some MSVC-specific passes / rewritings / diagnostics. *)
 
diff --git a/lib/Driver.ml b/lib/Driver.ml
index b46b0dd33..43a470497 100644
--- a/lib/Driver.ml
+++ b/lib/Driver.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** A very boring module that detects the environment and figures out how to
  * call the tools. *)
diff --git a/lib/Drop.ml b/lib/Drop.ml
index 47185e15f..466841bd8 100644
--- a/lib/Drop.ml
+++ b/lib/Drop.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 let file name =
   List.exists (fun p -> Bundle.pattern_matches_file p name) !Options.drop
diff --git a/lib/Error.ml b/lib/Error.ml
index cf7b9ec5d..513ece489 100644
--- a/lib/Error.ml
+++ b/lib/Error.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 open Ast
 
diff --git a/lib/Flags.ml b/lib/Flags.ml
index b57ed58d3..9e8a47eb0 100644
--- a/lib/Flags.ml
+++ b/lib/Flags.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 type flag =
   CError | CWarning | CSilent
diff --git a/lib/GcTypes.ml b/lib/GcTypes.ml
index 1defd4d88..8a011147b 100644
--- a/lib/GcTypes.ml
+++ b/lib/GcTypes.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Transformations specifically in support of types marked as GcType. We
  * essentially heap-allocate every constructor, then make sure that destructors
diff --git a/lib/GenCtypes.ml b/lib/GenCtypes.ml
index a09b74f02..b9332bced 100644
--- a/lib/GenCtypes.ml
+++ b/lib/GenCtypes.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Generating Ctypes OCaml bindings for C declarations *)
 
diff --git a/lib/GlobalNames.ml b/lib/GlobalNames.ml
index 4d147c3f5..95f412fa3 100644
--- a/lib/GlobalNames.ml
+++ b/lib/GlobalNames.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** All global names must be valid C identifiers and globally-unique... *)
 
diff --git a/lib/GlobalNames.mli b/lib/GlobalNames.mli
index 610e2005a..2e1726eec 100644
--- a/lib/GlobalNames.mli
+++ b/lib/GlobalNames.mli
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 type t
 
diff --git a/lib/Helpers.ml b/lib/Helpers.ml
index 3282348f3..b39e5c571 100644
--- a/lib/Helpers.ml
+++ b/lib/Helpers.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** A bunch of little helpers to deal with our AST. *)
 
diff --git a/lib/Idents.ml b/lib/Idents.ml
index 4e2d347d2..ddcccfd2b 100644
--- a/lib/Idents.ml
+++ b/lib/Idents.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Manipulation of identifiers *)
 
diff --git a/lib/Inlining.ml b/lib/Inlining.ml
index 3e2ac968e..a289147c6 100644
--- a/lib/Inlining.ml
+++ b/lib/Inlining.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Whole-program inlining based on the [MustDisappear] flag passed by F*. *)
 
diff --git a/lib/InputAst.ml b/lib/InputAst.ml
index b4874922c..33348b09a 100644
--- a/lib/InputAst.ml
+++ b/lib/InputAst.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Definition of the input format. *)
 
diff --git a/lib/InputAstToAst.ml b/lib/InputAstToAst.ml
index e67a0e4b8..f285e0053 100644
--- a/lib/InputAstToAst.ml
+++ b/lib/InputAstToAst.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** The translation from the input AST to the internal one. *)
 
diff --git a/lib/Loc.ml b/lib/Loc.ml
index 190c82fa4..ab5fa8f45 100644
--- a/lib/Loc.ml
+++ b/lib/Loc.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Helpers ----------------------------------------------------------------- *)
 
diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml
index 0b70f8573..ec9d10322 100644
--- a/lib/Monomorphization.ml
+++ b/lib/Monomorphization.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Monomorphization of functions and data types. *)
 
diff --git a/lib/OptimizeWasm.ml b/lib/OptimizeWasm.ml
index d333f4c91..c4be50efd 100644
--- a/lib/OptimizeWasm.ml
+++ b/lib/OptimizeWasm.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Minimal cleanups on the generated Wasm code to compensate for our naïve
  * compilation scheme. *)
diff --git a/lib/Options.ml b/lib/Options.ml
index 144f0dceb..904643c18 100644
--- a/lib/Options.ml
+++ b/lib/Options.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 type include_ = All | HeaderOnly of string | COnly of string
 
diff --git a/lib/Output.ml b/lib/Output.ml
index e7d0d02dd..0ae202229 100644
--- a/lib/Output.ml
+++ b/lib/Output.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Decorate each file with a little bit of boilerplate, then print it *)
 
diff --git a/lib/OutputJs.ml b/lib/OutputJs.ml
index 7ffc017ce..9fc9e7709 100644
--- a/lib/OutputJs.ml
+++ b/lib/OutputJs.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Output a set of Wasm files, along with toplevel entry files (HTML for a
  * browser, .js for a shell). *)
diff --git a/lib/Parsers.ml b/lib/Parsers.ml
index 6c76e62c9..00c2cf519 100644
--- a/lib/Parsers.ml
+++ b/lib/Parsers.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Just some handy shortcuts in a separate module to avoid complexity in the
  * dependency graph. *)
diff --git a/lib/Print.ml b/lib/Print.ml
index 973f8628d..81a9cc785 100644
--- a/lib/Print.ml
+++ b/lib/Print.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 let render doc =
   let buf = Buffer.create 1024 in
diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml
index e32b93392..0d743ccfd 100644
--- a/lib/PrintAst.ml
+++ b/lib/PrintAst.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* A pretty-printer for ASTs *)
 open PPrint
diff --git a/lib/PrintC.ml b/lib/PrintC.ml
index 0f72c637c..7c07e790a 100644
--- a/lib/PrintC.ml
+++ b/lib/PrintC.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Pretty-printer that conforms with C syntax. Also defines the grammar of
  * concrete C syntax, as opposed to our idealistic, well-formed C*. *)
diff --git a/lib/PrintCommon.ml b/lib/PrintCommon.ml
index be3eef09f..142547694 100644
--- a/lib/PrintCommon.ml
+++ b/lib/PrintCommon.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 open PPrint
 open Constant
diff --git a/lib/Simplify.ml b/lib/Simplify.ml
index 0534e2d96..ea2b0749b 100644
--- a/lib/Simplify.ml
+++ b/lib/Simplify.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** This module rewrites the original AST to send it into Low*, the subset we
  * know how to translate to C. *)
diff --git a/lib/SimplifyC89.ml b/lib/SimplifyC89.ml
index f38f7060d..39feea898 100644
--- a/lib/SimplifyC89.ml
+++ b/lib/SimplifyC89.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* A set of transformations for the sole purpose of bringing us closer to C89
  * compatibility. *)
diff --git a/lib/SimplifyMerge.ml b/lib/SimplifyMerge.ml
index 09661fb23..b197bab20 100644
--- a/lib/SimplifyMerge.ml
+++ b/lib/SimplifyMerge.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Merging variables together to avoid un-necessary let-bindings *)
 
diff --git a/lib/SimplifyWasm.ml b/lib/SimplifyWasm.ml
index 5310420c9..e7e3a9cac 100644
--- a/lib/SimplifyWasm.ml
+++ b/lib/SimplifyWasm.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (* Wasm-specific transformations that we perform now **************************)
 
diff --git a/lib/Structs.ml b/lib/Structs.ml
index bc05d5515..cfda41213 100644
--- a/lib/Structs.ml
+++ b/lib/Structs.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Make sure all structures are passed by reference  **************************)
 
diff --git a/lib/UseAnalysis.ml b/lib/UseAnalysis.ml
index 9bf6fea31..ae606095c 100644
--- a/lib/UseAnalysis.ml
+++ b/lib/UseAnalysis.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 open Ast
 open DeBruijn
diff --git a/lib/Warn.ml b/lib/Warn.ml
index 1941c30e6..a511e9331 100644
--- a/lib/Warn.ml
+++ b/lib/Warn.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** Unified warning handling *)
 
diff --git a/src/Karamel.ml b/src/Karamel.ml
index a7568766f..e524f98b4 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -1,5 +1,5 @@
 (* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
-(* Licensed under the Apache 2.0 License. *)
+(* Licensed under the Apache 2.0 and MIT Licenses. *)
 
 (** KaRaMeL, a tool to translate from a minimal ML-like language to C. *)