license under MIT license

LICENSE

@@ -0,0 +1,21 @@
+The MIT License (MIT)
+
+Copyright (c) 2024 Åsmund Kløvstad, Karl Palmskog
+
+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.

README.md

@@ -19,6 +19,7 @@ Formal metatheory in Coq for the ABS language.
 - Author(s):
   - Åsmund Kløvstad
   - Karl Palmskog
+- License: [MIT License](LICENSE)
 - Compatible Coq versions: 8.16 or later
 - Additional dependencies:
   - [Ott Coq library](https://github.com/ott-lang/ott) 0.33 or later

coq-abs-metatheory.opam

@@ -8,7 +8,7 @@ version: "dev"
 homepage: "https://github.com/kth-step/abs-metatheory"
 dev-repo: "git+https://github.com/kth-step/abs-metatheory.git"
 bug-reports: "https://github.com/kth-step/abs-metatheory/issues"
-
+license: "MIT"
 
 synopsis: "Formal metatheory in Coq of the ABS language"
 description: """

meta.yml

@@ -23,6 +23,10 @@ opam-file-maintainer: palmskog@gmail.com
 
 opam-file-version: dev
 
+license:
+  fullname: MIT License
+  identifier: MIT
+
 supported_coq_versions:
   text: 8.16 or later
   opam: '{>= "8.16"}'