Skip to content

Commit 65a16b9

Browse files
committed
Link to hash-stable released tarballs in all non-alphas metacoq packages
1 parent 0031f9b commit 65a16b9

File tree

114 files changed

+228
-228
lines changed
  • released/packages
    • coq-metacoq
      • coq-metacoq.1.0+8.14
      • coq-metacoq.1.0+8.15
      • coq-metacoq.1.0+8.16
      • coq-metacoq.1.1+8.14
      • coq-metacoq.1.1+8.15
      • coq-metacoq.1.1+8.16
      • coq-metacoq.1.1.1+8.14
      • coq-metacoq.1.1.1+8.15
      • coq-metacoq.1.1.1+8.16
      • coq-metacoq.1.2+8.16
      • coq-metacoq.1.2+8.17
      • coq-metacoq.1.2.1+8.17
      • coq-metacoq.1.2.1+8.18
      • coq-metacoq.1.3+8.17
    • coq-metacoq-common
      • coq-metacoq-common.1.2+8.16
      • coq-metacoq-common.1.2+8.17
      • coq-metacoq-common.1.2.1+8.17
      • coq-metacoq-common.1.2.1+8.18
      • coq-metacoq-common.1.3+8.17
    • coq-metacoq-erasure
      • coq-metacoq-erasure.1.0+8.14
      • coq-metacoq-erasure.1.0+8.15
      • coq-metacoq-erasure.1.0+8.16
      • coq-metacoq-erasure.1.1+8.14
      • coq-metacoq-erasure.1.1+8.15
      • coq-metacoq-erasure.1.1+8.16
      • coq-metacoq-erasure.1.1.1+8.14
      • coq-metacoq-erasure.1.1.1+8.15
      • coq-metacoq-erasure.1.1.1+8.16
      • coq-metacoq-erasure.1.2+8.16
      • coq-metacoq-erasure.1.2+8.17
      • coq-metacoq-erasure.1.2.1+8.17
      • coq-metacoq-erasure.1.2.1+8.18
      • coq-metacoq-erasure.1.3+8.17
    • coq-metacoq-erasure-plugin
      • coq-metacoq-erasure-plugin.1.2+8.16
      • coq-metacoq-erasure-plugin.1.2+8.17
      • coq-metacoq-erasure-plugin.1.2.1+8.17
      • coq-metacoq-erasure-plugin.1.2.1+8.18
      • coq-metacoq-erasure-plugin.1.3+8.17
    • coq-metacoq-pcuic
      • coq-metacoq-pcuic.1.0+8.14
      • coq-metacoq-pcuic.1.0+8.15
      • coq-metacoq-pcuic.1.0+8.16
      • coq-metacoq-pcuic.1.1+8.14
      • coq-metacoq-pcuic.1.1+8.15
      • coq-metacoq-pcuic.1.1+8.16
      • coq-metacoq-pcuic.1.1.1+8.14
      • coq-metacoq-pcuic.1.1.1+8.15
      • coq-metacoq-pcuic.1.1.1+8.16
      • coq-metacoq-pcuic.1.2+8.16
      • coq-metacoq-pcuic.1.2+8.17
      • coq-metacoq-pcuic.1.2.1+8.17
      • coq-metacoq-pcuic.1.2.1+8.18
      • coq-metacoq-pcuic.1.3+8.17
    • coq-metacoq-quotation
      • coq-metacoq-quotation.1.2+8.16
      • coq-metacoq-quotation.1.2+8.17
      • coq-metacoq-quotation.1.2.1+8.17
      • coq-metacoq-quotation.1.2.1+8.18
      • coq-metacoq-quotation.1.3+8.17
    • coq-metacoq-safechecker
      • coq-metacoq-safechecker.1.0+8.14
      • coq-metacoq-safechecker.1.0+8.15
      • coq-metacoq-safechecker.1.0+8.16
      • coq-metacoq-safechecker.1.1+8.14
      • coq-metacoq-safechecker.1.1+8.15
      • coq-metacoq-safechecker.1.1+8.16
      • coq-metacoq-safechecker.1.1.1+8.14
      • coq-metacoq-safechecker.1.1.1+8.15
      • coq-metacoq-safechecker.1.1.1+8.16
      • coq-metacoq-safechecker.1.2+8.16
      • coq-metacoq-safechecker.1.2+8.17
      • coq-metacoq-safechecker.1.2.1+8.17
      • coq-metacoq-safechecker.1.2.1+8.18
      • coq-metacoq-safechecker.1.3+8.17
    • coq-metacoq-safechecker-plugin
      • coq-metacoq-safechecker-plugin.1.2+8.16
      • coq-metacoq-safechecker-plugin.1.2+8.17
      • coq-metacoq-safechecker-plugin.1.2.1+8.17
      • coq-metacoq-safechecker-plugin.1.2.1+8.18
      • coq-metacoq-safechecker-plugin.1.3+8.17
    • coq-metacoq-template
      • coq-metacoq-template.1.0+8.14
      • coq-metacoq-template.1.0+8.15
      • coq-metacoq-template.1.0+8.16
      • coq-metacoq-template.1.1+8.14
      • coq-metacoq-template.1.1+8.15
      • coq-metacoq-template.1.1+8.16
      • coq-metacoq-template.1.1.1+8.14
      • coq-metacoq-template.1.1.1+8.15
      • coq-metacoq-template.1.1.1+8.16
      • coq-metacoq-template.1.2+8.16
      • coq-metacoq-template.1.2+8.17
      • coq-metacoq-template.1.2.1+8.17
      • coq-metacoq-template.1.2.1+8.18
      • coq-metacoq-template.1.3+8.17
    • coq-metacoq-template-pcuic
      • coq-metacoq-template-pcuic.1.2+8.16
      • coq-metacoq-template-pcuic.1.2+8.17
      • coq-metacoq-template-pcuic.1.2.1+8.17
      • coq-metacoq-template-pcuic.1.2.1+8.18
      • coq-metacoq-template-pcuic.1.3+8.17
    • coq-metacoq-translations
      • coq-metacoq-translations.1.0+8.14
      • coq-metacoq-translations.1.0+8.15
      • coq-metacoq-translations.1.0+8.16
      • coq-metacoq-translations.1.1+8.14
      • coq-metacoq-translations.1.1+8.15
      • coq-metacoq-translations.1.1+8.16
      • coq-metacoq-translations.1.1.1+8.14
      • coq-metacoq-translations.1.1.1+8.15
      • coq-metacoq-translations.1.1.1+8.16
      • coq-metacoq-translations.1.2+8.16
      • coq-metacoq-translations.1.2+8.17
      • coq-metacoq-translations.1.2.1+8.17
      • coq-metacoq-translations.1.2.1+8.18
      • coq-metacoq-translations.1.3+8.17
    • coq-metacoq-utils
      • coq-metacoq-utils.1.2+8.16
      • coq-metacoq-utils.1.2+8.17
      • coq-metacoq-utils.1.2.1+8.17
      • coq-metacoq-utils.1.2.1+8.18
      • coq-metacoq-utils.1.3+8.17

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

114 files changed

+228
-228
lines changed

Diff for: released/packages/coq-metacoq-common/coq-metacoq-common.1.2+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,6 @@ description: """
3434
MetaCoq is a meta-programming framework for Coq.
3535
"""
3636
url {
37-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.16.tar.gz"
38-
checksum: "sha512=1fc976740f2ff5a6c4137cf4722e09cae5765d0d71f55e6a020883218396856558a6534aa7d2bd192b60778427edbbc2f096a0e738e95551808702613edbbb31"
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2-8.16/metacoq-1.2-8.16.tar.gz"
38+
checksum: "sha512=80739c1424f5c28afadfcc581fa7016bc26f28f3a8b79597abc52ba5cc404cbe3728cccb260ab5ff7ed71ecb9a66690bcaa8d9cc6c0b79d2d1b5e660c34d5008"
3939
}

Diff for: released/packages/coq-metacoq-common/coq-metacoq-common.1.2+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,6 @@ description: """
3434
MetaCoq is a meta-programming framework for Coq.
3535
"""
3636
url {
37-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.17.tar.gz"
38-
checksum: "sha512=a5ce2f5d94120a00703331a3cfdb7d51653fb44adeba89fa84b5f76e711ee9f582a22551f81fd144dc974e3f05e58d85cd716f8fcf69ec89923bc64774d82668"
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2-8.17/metacoq-1.2-8.17.tar.gz"
38+
checksum: "sha512=ef36dfe0e7864c67e223484f400f38531b41059c6e6e206a329b4dfa2c29e36ee133a711656fec3edcb37b046e5602d1a81c9989c399729f4547f19e854ccdbd"
3939
}

Diff for: released/packages/coq-metacoq-common/coq-metacoq-common.1.2.1+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,6 @@ description: """
3434
MetaCoq is a meta-programming framework for Coq.
3535
"""
3636
url {
37-
src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.17.tar.gz"
38-
checksum: "sha256=cfa174fbf9241e9a19240982a33015e9562f221cbb228d04995881f5f2086488"
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2.1-8.17/metacoq-1.2.1-8.17.tar.gz"
38+
checksum: "sha512=c02f106aafa1082bb6c2be5bb1c972840cd23d94c85541996767855e1a3080bc00405f463d275285847385680aa69b3798d067ed73e4712d8a137024cc256cab"
3939
}

Diff for: released/packages/coq-metacoq-common/coq-metacoq-common.1.2.1+8.18/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,6 @@ description: """
3434
MetaCoq is a meta-programming framework for Coq.
3535
"""
3636
url {
37-
src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.18.tar.gz"
38-
checksum: "sha256=dd129826edd22e611f84cdc82f6486fc57343e13c8223ce041a3d0574b6f5262"
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2.1-8.18/metacoq-1.2.1-8.18.tar.gz"
38+
checksum: "sha512=3b2a6c1cb8005a7f675c47209b17f0b3f2ded6b3ae324f6a6782f0b23e5e5e5e25ac1d1c8a97be1c9b89b4490dda80567a3f57c254314a185a01ca9f0fc94d82"
3939
}

Diff for: released/packages/coq-metacoq-common/coq-metacoq-common.1.3+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,6 @@ description: """
3434
MetaCoq is a meta-programming framework for Coq.
3535
"""
3636
url {
37-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3-8.17.tar.gz"
38-
checksum: "sha512=75526a9c5bfbd71996a00d05a707f8fd5c26469f8ce79127bb6cc031b9d773dff639c8605f604f5a1fc1f3e16792e812150b79efe9a249985fc68192ba38e651"
37+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.3-8.17/metacoq-1.3-8.17.tar.gz"
38+
checksum: "sha512=eef100ec9a30031d99e8f626f00fbd4d3156bc64e440086876c13490207e6fd845cf9c0688dc417feb4f4acd1c9ca7f3d467dd3250319090250c926e7c62fba0"
3939
}

Diff for: released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.2+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.16.tar.gz"
47-
checksum: "sha512=1fc976740f2ff5a6c4137cf4722e09cae5765d0d71f55e6a020883218396856558a6534aa7d2bd192b60778427edbbc2f096a0e738e95551808702613edbbb31"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2-8.16/metacoq-1.2-8.16.tar.gz"
47+
checksum: "sha512=80739c1424f5c28afadfcc581fa7016bc26f28f3a8b79597abc52ba5cc404cbe3728cccb260ab5ff7ed71ecb9a66690bcaa8d9cc6c0b79d2d1b5e660c34d5008"
4848
}

Diff for: released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.2+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.17.tar.gz"
47-
checksum: "sha512=a5ce2f5d94120a00703331a3cfdb7d51653fb44adeba89fa84b5f76e711ee9f582a22551f81fd144dc974e3f05e58d85cd716f8fcf69ec89923bc64774d82668"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2-8.17/metacoq-1.2-8.17.tar.gz"
47+
checksum: "sha512=ef36dfe0e7864c67e223484f400f38531b41059c6e6e206a329b4dfa2c29e36ee133a711656fec3edcb37b046e5602d1a81c9989c399729f4547f19e854ccdbd"
4848
}

Diff for: released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.2.1+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.17.tar.gz"
47-
checksum: "sha256=cfa174fbf9241e9a19240982a33015e9562f221cbb228d04995881f5f2086488"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2.1-8.17/metacoq-1.2.1-8.17.tar.gz"
47+
checksum: "sha512=c02f106aafa1082bb6c2be5bb1c972840cd23d94c85541996767855e1a3080bc00405f463d275285847385680aa69b3798d067ed73e4712d8a137024cc256cab"
4848
}

Diff for: released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.2.1+8.18/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.18.tar.gz"
47-
checksum: "sha256=dd129826edd22e611f84cdc82f6486fc57343e13c8223ce041a3d0574b6f5262"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2.1-8.18/metacoq-1.2.1-8.18.tar.gz"
47+
checksum: "sha512=3b2a6c1cb8005a7f675c47209b17f0b3f2ded6b3ae324f6a6782f0b23e5e5e5e25ac1d1c8a97be1c9b89b4490dda80567a3f57c254314a185a01ca9f0fc94d82"
4848
}

Diff for: released/packages/coq-metacoq-erasure-plugin/coq-metacoq-erasure-plugin.1.3+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3-8.17.tar.gz"
47-
checksum: "sha512=75526a9c5bfbd71996a00d05a707f8fd5c26469f8ce79127bb6cc031b9d773dff639c8605f604f5a1fc1f3e16792e812150b79efe9a249985fc68192ba38e651"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.3-8.17/metacoq-1.3-8.17.tar.gz"
47+
checksum: "sha512=eef100ec9a30031d99e8f626f00fbd4d3156bc64e440086876c13490207e6fd845cf9c0688dc417feb4f4acd1c9ca7f3d467dd3250319090250c926e7c62fba0"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.0+8.14/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.14.tar.gz"
47-
checksum: "sha512=0dffdc83c156484b67b70ff7e15178f351af9650c4576bc408ccc370d61dac255f5d47bd50310a50fb29ee0d3df7b7250cf6b79ad8e351fe1310c4c1f86ed624"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.0-8.14/metacoq-1.0-8.14.tar.gz"
47+
checksum: "sha512=208a6ba9ca2f2e4b9968baca059e5c290d22d083c30591c53b70275b82478510327c27cd6980ddae6245e491a976ffcbbfa4d004767e6dc172a88f042f921698"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.0+8.15/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.15.tar.gz"
47-
checksum: "sha512=b52d833e9d7a442f6b4caa6d710d7cb0fb63e0f8fe39d7d67b7c9f5cd5ff05f49779ecd84aeb594534642102a723c5f009fabaea78127883d63cfafd0270b8e4"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.0-8.15/metacoq-1.0-8.15.tar.gz"
47+
checksum: "sha512=8bf61d638afcefa661f65a3e7384fdffef358bed4985a9df8d60dc200603172d1931ad94cbc028e82ba9b44778f59428e240e02642111765a4470a1202264224"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.0+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4242
thesis.
4343
"""
4444
url {
45-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz"
46-
checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593"
45+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.0-8.16/metacoq-1.0-8.16.tar.gz"
46+
checksum: "sha512=44f9364cfb0a2995e0adadbdb181e53a1dccd98781ab1b9abdde7942ee4b15ea233bca97c28e3185c8492a8af7db7cfe57e34d535b94d5465b9f3c3c5eb3f4e7"
4747
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.1+8.14/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.14.tar.gz"
47-
checksum: "sha512=7a0c4ca2e434ecd325a4d11a235ea11c77a8533aafb5119546d4fbc518308d0c760865bb63ff6807f18916738af79636f5c89fcf32eed8e45dde08ac92011d0c"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1-8.14/metacoq-1.1-8.14.tar.gz"
47+
checksum: "sha512=e5cc8a540c7a7bb2a783c41ed6f6808362bf27c781fbb1f609e2b8da881065eba7adb74cf99132aa40329f88fec7547e79a6fdef268e609604cf35e82dc7ee6a"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.1+8.15/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.15.tar.gz"
47-
checksum: "sha512=e75c1171fb6a41b21fc5c3f8f788698939dfa8abe950f16afaee2425426236e61be464f4eb69a2d36430fe6b51e980e83b97e88e58a1aa78ae253e249a49d49b"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1-8.15/metacoq-1.1-8.15.tar.gz"
47+
checksum: "sha512=ebb88e267033fc6167f41d51ccb233c171eb70775ba3b04aa3c7517ff073be31dcdf331e9901897d6c3e5893f6d12ec48d5851d44c23b1ec8c7e7d3d505eb360"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.1+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.16.tar.gz"
47-
checksum: "sha512=abd34042fc2804954abc8b1fba4c2b3d1d1c0c780874ad0cbe698a19756e26985c77bb231b2e9b40ea01261f3fbbb36fbdd2b7095931e947bf933359cb0154f7"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1-8.16/metacoq-1.1-8.16.tar.gz"
47+
checksum: "sha512=aa984b616d5e91a264e765973ef02d8c180da282d7c87017fc2ca7f783ed819f0f62f5f96c1cab7f11fc2993cbb424f48c4a00a0bcdf0c98f19460cd7dcce5aa"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.1.1+8.14/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.14.tar.gz"
47-
checksum: "sha512=90a4326e38d51ef188816784ed49bfce92eb4580cd32bc19776d13b91954e26592304b83f9d9d5370adcdc1f319381e105c3e69aed0756b070451ea0229d235a"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1.1-8.14/metacoq-1.1.1-8.14.tar.gz"
47+
checksum: "sha512=e54a9dc6a01dbe7c95343327e63eed8011366347bd02c29eca9426a6b8d955e5d0209df448e2f2fbb517e8b928f7d22276e55aae092bd3c4e9f4ba11bcac85c5"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.1.1+8.15/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.15.tar.gz"
47-
checksum: "sha512=83d6b109217139640a081a9ef98b35cf33b1f568b8941f0b23d43abd25d22331cee16fbdd77335583fe74fea0f28215facf1cd9cb416e460a785c6061a454bae"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1.1-8.15/metacoq-1.1.1-8.15.tar.gz"
47+
checksum: "sha512=651f6f59cae604169a8c2fef48df75324791adf1becd881b36f01c5bc407a6fef9209d69f4c917d72e8c86f06ae2db976cfed6778be438786b14ab6daf771c25"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.1.1+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.16.tar.gz"
47-
checksum: "sha512=82397806d842f0839eb82066ed5dfe9a54b49989ca7efdab8b861a8d8bea6ec3739746b0d338857d4df01790a636f106601ed8e01ebbf9b02e7e4e76ca47d6fe"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1.1-8.16/metacoq-1.1.1-8.16.tar.gz"
47+
checksum: "sha512=babae48068b31833a695ddbf7cac1043ccab778dcb5ea1cd6db3277f77f994a926636b10e58254615c88d080f69fc1885ea11d5bc8743e313e621aab2c9e48db"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.2+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.16.tar.gz"
47-
checksum: "sha512=1fc976740f2ff5a6c4137cf4722e09cae5765d0d71f55e6a020883218396856558a6534aa7d2bd192b60778427edbbc2f096a0e738e95551808702613edbbb31"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2-8.16/metacoq-1.2-8.16.tar.gz"
47+
checksum: "sha512=80739c1424f5c28afadfcc581fa7016bc26f28f3a8b79597abc52ba5cc404cbe3728cccb260ab5ff7ed71ecb9a66690bcaa8d9cc6c0b79d2d1b5e660c34d5008"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.2+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.2-8.17.tar.gz"
47-
checksum: "sha512=a5ce2f5d94120a00703331a3cfdb7d51653fb44adeba89fa84b5f76e711ee9f582a22551f81fd144dc974e3f05e58d85cd716f8fcf69ec89923bc64774d82668"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2-8.17/metacoq-1.2-8.17.tar.gz"
47+
checksum: "sha512=ef36dfe0e7864c67e223484f400f38531b41059c6e6e206a329b4dfa2c29e36ee133a711656fec3edcb37b046e5602d1a81c9989c399729f4547f19e854ccdbd"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.2.1+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.17.tar.gz"
47-
checksum: "sha256=cfa174fbf9241e9a19240982a33015e9562f221cbb228d04995881f5f2086488"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2.1-8.17/metacoq-1.2.1-8.17.tar.gz"
47+
checksum: "sha512=c02f106aafa1082bb6c2be5bb1c972840cd23d94c85541996767855e1a3080bc00405f463d275285847385680aa69b3798d067ed73e4712d8a137024cc256cab"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.2.1+8.18/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/v1.2.1-8.18.tar.gz"
47-
checksum: "sha256=dd129826edd22e611f84cdc82f6486fc57343e13c8223ce041a3d0574b6f5262"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.2.1-8.18/metacoq-1.2.1-8.18.tar.gz"
47+
checksum: "sha512=3b2a6c1cb8005a7f675c47209b17f0b3f2ded6b3ae324f6a6782f0b23e5e5e5e25ac1d1c8a97be1c9b89b4490dda80567a3f57c254314a185a01ca9f0fc94d82"
4848
}

Diff for: released/packages/coq-metacoq-erasure/coq-metacoq-erasure.1.3+8.17/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,6 @@ into a dummy `tBox` constructor, following closely P. Letouzey's PhD
4343
thesis.
4444
"""
4545
url {
46-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.3-8.17.tar.gz"
47-
checksum: "sha512=75526a9c5bfbd71996a00d05a707f8fd5c26469f8ce79127bb6cc031b9d773dff639c8605f604f5a1fc1f3e16792e812150b79efe9a249985fc68192ba38e651"
46+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.3-8.17/metacoq-1.3-8.17.tar.gz"
47+
checksum: "sha512=eef100ec9a30031d99e8f626f00fbd4d3156bc64e440086876c13490207e6fd845cf9c0688dc417feb4f4acd1c9ca7f3d467dd3250319090250c926e7c62fba0"
4848
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.0+8.14/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3838
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3939
"""
4040
url {
41-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.14.tar.gz"
42-
checksum: "sha512=0dffdc83c156484b67b70ff7e15178f351af9650c4576bc408ccc370d61dac255f5d47bd50310a50fb29ee0d3df7b7250cf6b79ad8e351fe1310c4c1f86ed624"
41+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.0-8.14/metacoq-1.0-8.14.tar.gz"
42+
checksum: "sha512=208a6ba9ca2f2e4b9968baca059e5c290d22d083c30591c53b70275b82478510327c27cd6980ddae6245e491a976ffcbbfa4d004767e6dc172a88f042f921698"
4343
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.0+8.15/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3737
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3838
"""
3939
url {
40-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.15.tar.gz"
41-
checksum: "sha512=b52d833e9d7a442f6b4caa6d710d7cb0fb63e0f8fe39d7d67b7c9f5cd5ff05f49779ecd84aeb594534642102a723c5f009fabaea78127883d63cfafd0270b8e4"
40+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.0-8.15/metacoq-1.0-8.15.tar.gz"
41+
checksum: "sha512=8bf61d638afcefa661f65a3e7384fdffef358bed4985a9df8d60dc200603172d1931ad94cbc028e82ba9b44778f59428e240e02642111765a4470a1202264224"
4242
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.0+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3636
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3737
"""
3838
url {
39-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.0-8.16.tar.gz"
40-
checksum: "sha512=84c59b74d7ed3798593026d00e412ce2a9d1443afdaf98f5f680788ed8e73cf7e67dcd91392efe2243c5cd61b979edea9bf109f72ea5c45de5c31ef732bba593"
39+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.0-8.16/metacoq-1.0-8.16.tar.gz"
40+
checksum: "sha512=44f9364cfb0a2995e0adadbdb181e53a1dccd98781ab1b9abdde7942ee4b15ea233bca97c28e3185c8492a8af7db7cfe57e34d535b94d5465b9f3c3c5eb3f4e7"
4141
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.1+8.14/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3838
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3939
"""
4040
url {
41-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.14.tar.gz"
42-
checksum: "sha512=7a0c4ca2e434ecd325a4d11a235ea11c77a8533aafb5119546d4fbc518308d0c760865bb63ff6807f18916738af79636f5c89fcf32eed8e45dde08ac92011d0c"
41+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1-8.14/metacoq-1.1-8.14.tar.gz"
42+
checksum: "sha512=e5cc8a540c7a7bb2a783c41ed6f6808362bf27c781fbb1f609e2b8da881065eba7adb74cf99132aa40329f88fec7547e79a6fdef268e609604cf35e82dc7ee6a"
4343
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.1+8.15/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3737
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3838
"""
3939
url {
40-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.15.tar.gz"
41-
checksum: "sha512=e75c1171fb6a41b21fc5c3f8f788698939dfa8abe950f16afaee2425426236e61be464f4eb69a2d36430fe6b51e980e83b97e88e58a1aa78ae253e249a49d49b"
40+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1-8.15/metacoq-1.1-8.15.tar.gz"
41+
checksum: "sha512=ebb88e267033fc6167f41d51ccb233c171eb70775ba3b04aa3c7517ff073be31dcdf331e9901897d6c3e5893f6d12ec48d5851d44c23b1ec8c7e7d3d505eb360"
4242
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.1+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3737
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3838
"""
3939
url {
40-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1-8.16.tar.gz"
41-
checksum: "sha512=abd34042fc2804954abc8b1fba4c2b3d1d1c0c780874ad0cbe698a19756e26985c77bb231b2e9b40ea01261f3fbbb36fbdd2b7095931e947bf933359cb0154f7"
40+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1-8.16/metacoq-1.1-8.16.tar.gz"
41+
checksum: "sha512=aa984b616d5e91a264e765973ef02d8c180da282d7c87017fc2ca7f783ed819f0f62f5f96c1cab7f11fc2993cbb424f48c4a00a0bcdf0c98f19460cd7dcce5aa"
4242
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.1.1+8.14/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3838
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3939
"""
4040
url {
41-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.14.tar.gz"
42-
checksum: "sha512=90a4326e38d51ef188816784ed49bfce92eb4580cd32bc19776d13b91954e26592304b83f9d9d5370adcdc1f319381e105c3e69aed0756b070451ea0229d235a"
41+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1.1-8.14/metacoq-1.1.1-8.14.tar.gz"
42+
checksum: "sha512=e54a9dc6a01dbe7c95343327e63eed8011366347bd02c29eca9426a6b8d955e5d0209df448e2f2fbb517e8b928f7d22276e55aae092bd3c4e9f4ba11bcac85c5"
4343
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.1.1+8.15/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3737
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3838
"""
3939
url {
40-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.15.tar.gz"
41-
checksum: "sha512=83d6b109217139640a081a9ef98b35cf33b1f568b8941f0b23d43abd25d22331cee16fbdd77335583fe74fea0f28215facf1cd9cb416e460a785c6061a454bae"
40+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1.1-8.15/metacoq-1.1.1-8.15.tar.gz"
41+
checksum: "sha512=651f6f59cae604169a8c2fef48df75324791adf1becd881b36f01c5bc407a6fef9209d69f4c917d72e8c86f06ae2db976cfed6778be438786b14ab6daf771c25"
4242
}

Diff for: released/packages/coq-metacoq-pcuic/coq-metacoq-pcuic.1.1.1+8.16/opam

+2-2
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,6 @@ with a certified typechecker for it. This module includes the standard metatheor
3737
PCUIC: Weakening, Substitution, Confluence and Subject Reduction are proven here.
3838
"""
3939
url {
40-
src: "https://github.com/MetaCoq/metacoq/archive/refs/tags/v1.1.1-8.16.tar.gz"
41-
checksum: "sha512=82397806d842f0839eb82066ed5dfe9a54b49989ca7efdab8b861a8d8bea6ec3739746b0d338857d4df01790a636f106601ed8e01ebbf9b02e7e4e76ca47d6fe"
40+
src: "https://github.com/MetaRocq/metarocq/releases/download/v1.1.1-8.16/metacoq-1.1.1-8.16.tar.gz"
41+
checksum: "sha512=babae48068b31833a695ddbf7cac1043ccab778dcb5ea1cd6db3277f77f994a926636b10e58254615c88d080f69fc1885ea11d5bc8743e313e621aab2c9e48db"
4242
}

0 commit comments

Comments
 (0)