diff --git a/LICENSE.md b/LICENSE.md
new file mode 100644
index 0000000000000000000000000000000000000000..884314c4cd0b7bf0e68fda6ad7c3628f9da21ed7
--- /dev/null
+++ b/LICENSE.md
@@ -0,0 +1,3 @@
+# License
+
+<a rel="license" href="http://creativecommons.org/licenses/by/4.0/"><img alt="Creative Commons License" style="border-width:0" src="https://i.creativecommons.org/l/by/4.0/88x31.png" /></a><br /><span xmlns:dct="http://purl.org/dc/terms/" href="http://purl.org/dc/dcmitype/Text" property="dct:title" rel="dct:type">Prouvez que vos programmes fonctionnels n'ont pas de bugs avec Coq Première partie</span> by <span xmlns:cc="http://creativecommons.org/ns#" property="cc:attributionName">Yves Bertot</span> is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>.<br />Based on a work at <a xmlns:dct="http://purl.org/dc/terms/" href="https://gitlab.inria.fr/bertot/progcoq" rel="dct:source">https://gitlab.inria.fr/bertot/progcoq</a>.
\ No newline at end of file