diff --git a/bucket/coq.json b/bucket/coq.json
index 9f5002ca38..45354cd90f 100644
--- a/bucket/coq.json
+++ b/bucket/coq.json
@@ -2,7 +2,10 @@
     "version": "2022.01.0",
     "description": "A formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.",
     "homepage": "https://coq.inria.fr/",
-    "license": "LGPL-2.1-only",
+    "license": {
+        "identifier": "Proprietary, LGPL-2.1-only, LGPL-3.0-or-later, MIT, GPL-2.0-only, BSD-2-Clause-FreeBSD, CECILL-C, BSD-3-Clause, CECILL-B, ...",
+        "url": "https://github.com/AbsInt/CompCert/blob/master/LICENSE"
+    },
     "architecture": {
         "64bit": {
             "url": "https://github.com/coq/platform/releases/download/2022.01.0/Coq-Platform-8.14.2022.01-installer-windows-x86_64_signed.exe#/dl.7z",