diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam
deleted file mode 100644
index 4a72fb764f..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7/opam
+++ /dev/null
@@ -1,51 +0,0 @@
-opam-version: "2.0"
-authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-maintainer: "Jacques-Henri Jourdan <jacques-Henri.jourdan@normalesup.org>"
-homepage: "http://compcert.inria.fr/"
-dev-repo: "git+https://github.com/AbsInt/CompCert.git"
-bug-reports: "https://github.com/AbsInt/CompCert/issues"
-license: "INRIA Non-Commercial License Agreement"
-build: [
-  ["./configure" "amd64-linux" {os = "linux"}
-  "amd64-macosx" {os = "macos"}
-  "amd64-cygwin" {os = "cygwin"}
-  "-prefix" "%{prefix}%/variants/compcert64"
-  "-install-coqdev"
-  "-clightgen"
-  "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert"
-  "-ignore-coq-version"]
-  [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
-]
-install: [
-  [make "install"]
-]
-depends: [
-  "coq" {>= "8.7.0" & < "8.12"}
-  "menhir" {>= "20190626" & < "20200123"}
-  "ocaml" {>= "4.05.0"}
-]
-synopsis: "The CompCert C compiler (64 bit)"
-description: "This package installs the 64 bit version of CompCert.
-For coexistence with the 32 bit version, the files are installed in:
-%{prefix}%/variants/compcert64/bin  (ccomp and clightgen binaries)
-%{prefix}%/variants/compcert64/lib/compcert  (C library)
-%{lib}%/coq/user-contrib/compcert64  (Coq library)
-Please note that the coq module path is compcert and not compcert64,
-so the files cannot be directly Required as compcert64.
-Instead -Q or -R options must be used to bind the compcert64 folder
-to the module path compcert. This is more convenient if one development
-uses both 32 and 64 bit versions. Otherwise all files would have to
-be duplicated with module paths compcert and compcert64.
-Please also note that the binary folder is usually not in the path."
-tags: [
-  "category:CS/Semantics and Compilation/Compilation"
-  "category:CS/Semantics and Compilation/Semantics"
-  "keyword:C"
-  "keyword:compiler"
-  "logpath:compcert64"
-  "date:2020-03-21"
-]
-url {
-  src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz"
-  checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0"
-}
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
deleted file mode 100644
index d160e66e23..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
+++ /dev/null
@@ -1,82 +0,0 @@
-From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001
-From: Xavier Leroy <xavier.leroy@college-de-france.fr>
-Date: Wed, 29 Apr 2020 15:40:13 +0200
-Subject: [PATCH 01/12] Install "compcert.config" file along the Coq
- development
-
-The file contains various parameters about the target processor and ABI,
-useful for VST and possibly other users of CompCert as a Coq library.
-
-It is in "var=val" syntax so that it can be included directly from
-a Makefile or a shell script.
----
- .gitignore |  1 +
- Makefile   | 19 ++++++++++++++++++-
- 2 files changed, 19 insertions(+), 1 deletion(-)
-
-diff --git a/.gitignore b/.gitignore
-index 6c10e1c3..b75ea5e7 100644
---- a/.gitignore
-+++ b/.gitignore
-@@ -31,6 +31,7 @@
- /.depend
- /.depend.extr
- /compcert.ini
-+/compcert.config
- /x86/ConstpropOp.v
- /x86/SelectOp.v
- /x86/SelectLong.v
-diff --git a/Makefile b/Makefile
-index aed0da28..df5fb03f 100644
---- a/Makefile
-+++ b/Makefile
-@@ -147,6 +147,9 @@ endif
- ifeq ($(CLIGHTGEN),true)
- 	$(MAKE) clightgen
- endif
-+ifeq ($(INSTALL_COQDEV),true)
-+	$(MAKE) compcert.config
-+endif
- 
- proof: $(FILES:.v=.vo)
- 
-@@ -224,6 +227,19 @@ compcert.ini: Makefile.config
- 	 echo "response_file_style=$(RESPONSEFILE)";) \
-         > compcert.ini
- 
-+compcert.config: Makefile.config
-+	(echo "# CompCert configuration parameters"; \
-+        echo "COMPCERT_ARCH=$(ARCH)"; \
-+        echo "COMPCERT_MODEL=$(MODEL)"; \
-+        echo "COMPCERT_ABI=$(ABI)"; \
-+        echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \
-+        echo "COMPCERT_BITSIZE=$(BITSIZE)"; \
-+        echo "COMPCERT_SYSTEM=$(SYSTEM)"; \
-+        echo "COMPCERT_VERSION=$(BUILDVERSION)"; \
-+        echo "COMPCERT_BUILDNR=$(BUILDNR)"; \
-+        echo "COMPCERT_TAG=$(TAG)" \
-+        ) > compcert.config
-+
- driver/Version.ml: VERSION
- 	(echo 'let version = "$(BUILDVERSION)"'; \
-          echo 'let buildnr = "$(BUILDNR)"'; \
-@@ -258,6 +274,7 @@ ifeq ($(INSTALL_COQDEV),true)
-           install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
- 	done
- 	install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
-+	install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
- 	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
- endif
- 
-@@ -267,7 +284,7 @@ clean:
- 	rm -f $(patsubst %, %/.*.aux, $(DIRS))
- 	rm -rf doc/html doc/*.glob
- 	rm -f driver/Version.ml
--	rm -f compcert.ini
-+	rm -f compcert.ini compcert.config
- 	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
- 	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
- 	rm -f $(GENERATED) .depend
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
deleted file mode 100644
index f74202a53c..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
+++ /dev/null
@@ -1,60 +0,0 @@
-From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001
-From: Xavier Leroy <xavier.leroy@college-de-france.fr>
-Date: Sun, 3 May 2020 09:43:14 +0200
-Subject: [PATCH 07/12] Dual-license
- aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}
-
-The corresponding files in all other ports are dual-licensed
-(GPL + non-commercial), there is no reason it should be different for
-aarch64.
----
- aarch64/Archi.v             | 3 +++
- aarch64/CBuiltins.ml        | 3 +++
- aarch64/extractionMachdep.v | 3 +++
- 3 files changed, 9 insertions(+)
-
-diff --git a/aarch64/Archi.v b/aarch64/Archi.v
-index aef4ab77..24431cb2 100644
---- a/aarch64/Archi.v
-+++ b/aarch64/Archi.v
-@@ -6,6 +6,9 @@
- (*                                                                     *)
- (*  Copyright Institut National de Recherche en Informatique et en     *)
- (*  Automatique.  All rights reserved.  This file is distributed       *)
-+(*  under the terms of the GNU General Public License as published by  *)
-+(*  the Free Software Foundation, either version 2 of the License, or  *)
-+(*  (at your option) any later version.  This file is also distributed *)
- (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
- (*                                                                     *)
- (* *********************************************************************)
-diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml
-index fdc1372d..dfd5b768 100644
---- a/aarch64/CBuiltins.ml
-+++ b/aarch64/CBuiltins.ml
-@@ -6,6 +6,9 @@
- (*                                                                     *)
- (*  Copyright Institut National de Recherche en Informatique et en     *)
- (*  Automatique.  All rights reserved.  This file is distributed       *)
-+(*  under the terms of the GNU General Public License as published by  *)
-+(*  the Free Software Foundation, either version 2 of the License, or  *)
-+(*  (at your option) any later version.  This file is also distributed *)
- (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
- (*                                                                     *)
- (* *********************************************************************)
-diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
-index e82056e2..5f26dc28 100644
---- a/aarch64/extractionMachdep.v
-+++ b/aarch64/extractionMachdep.v
-@@ -6,6 +6,9 @@
- (*                                                                     *)
- (*  Copyright Institut National de Recherche en Informatique et en     *)
- (*  Automatique.  All rights reserved.  This file is distributed       *)
-+(*  under the terms of the GNU General Public License as published by  *)
-+(*  the Free Software Foundation, either version 2 of the License, or  *)
-+(*  (at your option) any later version.  This file is also distributed *)
- (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
- (*                                                                     *)
- (* *********************************************************************)
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch
deleted file mode 100644
index 57bef5e519..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0008-Update-the-list-of-dual-licensed-files.patch
+++ /dev/null
@@ -1,28 +0,0 @@
-From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001
-From: Xavier Leroy <xavier.leroy@college-de-france.fr>
-Date: Mon, 4 May 2020 10:51:47 +0200
-Subject: [PATCH 08/12] Update the list of dual-licensed files
-
-Closes: #351
----
- LICENSE | 4 ++--
- 1 file changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/LICENSE b/LICENSE
-index 5a7ae79f..61b84219 100644
---- a/LICENSE
-+++ b/LICENSE
-@@ -46,8 +46,8 @@ option) any later version:
- 
-   all files in the exportclight/ directory
- 
--  the Archi.v, CBuiltins.ml, and extractionMachdep.v files
--  in directories arm, powerpc, riscV, x86, x86_32, x86_64
-+  the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files
-+  in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64
- 
-   extraction/extraction.v
- 
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch
deleted file mode 100644
index 0dc512b457..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0011-Use-Coq-platform-supplied-Flocq.patch
+++ /dev/null
@@ -1,123 +0,0 @@
-From 05448adb7642b3c1189139cec18c914b116d5d40 Mon Sep 17 00:00:00 2001
-From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
-Date: Thu, 30 Apr 2020 16:25:19 +0200
-Subject: [PATCH 11/12] Use Coq platform supplied Flocq
-
----
- aarch64/Archi.v     | 2 +-
- arm/Archi.v         | 2 +-
- lib/Floats.v        | 2 +-
- lib/IEEE754_extra.v | 2 +-
- powerpc/Archi.v     | 2 +-
- riscV/Archi.v       | 2 +-
- x86_32/Archi.v      | 2 +-
- x86_64/Archi.v      | 2 +-
- 8 files changed, 8 insertions(+), 8 deletions(-)
-
-diff --git a/aarch64/Archi.v b/aarch64/Archi.v
-index 24431cb2..6c5655d8 100644
---- a/aarch64/Archi.v
-+++ b/aarch64/Archi.v
-@@ -16,7 +16,7 @@
- (** Architecture-dependent parameters for AArch64 *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := true.
-diff --git a/arm/Archi.v b/arm/Archi.v
-index 16d6c71d..9b4cc96a 100644
---- a/arm/Archi.v
-+++ b/arm/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for ARM *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := false.
-diff --git a/lib/Floats.v b/lib/Floats.v
-index 6a126c3f..25a55620 100644
---- a/lib/Floats.v
-+++ b/lib/Floats.v
-@@ -17,7 +17,7 @@
- (** Formalization of floating-point numbers, using the Flocq library. *)
- 
- Require Import Coqlib Zbits Integers.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits Core.
- Require Import IEEE754_extra.
- Require Import Program.
-diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
-index c23149be..d546c7d3 100644
---- a/lib/IEEE754_extra.v
-+++ b/lib/IEEE754_extra.v
-@@ -20,7 +20,7 @@
- Require Import Psatz.
- Require Import Bool.
- Require Import Eqdep_dec.
--(*From Flocq *)
-+From Flocq
- Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd.
- 
- Local Open Scope Z_scope.
-diff --git a/powerpc/Archi.v b/powerpc/Archi.v
-index 10f38391..5ada45f4 100644
---- a/powerpc/Archi.v
-+++ b/powerpc/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for PowerPC *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := false.
-diff --git a/riscV/Archi.v b/riscV/Archi.v
-index 61d129d0..4a929aac 100644
---- a/riscV/Archi.v
-+++ b/riscV/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for RISC-V *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Parameter ptr64 : bool.
-diff --git a/x86_32/Archi.v b/x86_32/Archi.v
-index e9d05c14..b5e4b638 100644
---- a/x86_32/Archi.v
-+++ b/x86_32/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for x86 in 32-bit mode *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := false.
-diff --git a/x86_64/Archi.v b/x86_64/Archi.v
-index 959d8dc1..59502b4a 100644
---- a/x86_64/Archi.v
-+++ b/x86_64/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for x86 in 64-bit mode *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := true.
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
deleted file mode 100644
index 58a641f077..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
+++ /dev/null
@@ -1,26 +0,0 @@
-From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001
-From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
-Date: Tue, 5 May 2020 17:10:06 +0200
-Subject: [PATCH 12/12] Use platform supplied menhirlib as suggested by
- jhjourdan
-
----
- Makefile | 2 +-
- 1 file changed, 1 insertion(+), 1 deletion(-)
-
-diff --git a/Makefile b/Makefile
-index 48770ebd..c4130630 100644
---- a/Makefile
-+++ b/Makefile
-@@ -265,7 +265,7 @@ driver/Version.ml: VERSION
- 
- cparser/Parser.v: cparser/Parser.vy
- 	@rm -f $@
--	$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
-+	$(MENHIR) --coq cparser/Parser.vy
- 	@chmod a-w $@
- 
- depend: $(GENERATED) depend1
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam
deleted file mode 100644
index 39e300c938..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform/opam
+++ /dev/null
@@ -1,68 +0,0 @@
-opam-version: "2.0"
-authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-maintainer: "Jacques-Henri Jourdan <jacques-Henri.jourdan@normalesup.org>"
-homepage: "http://compcert.inria.fr/"
-dev-repo: "git+https://github.com/AbsInt/CompCert.git"
-bug-reports: "https://github.com/AbsInt/CompCert/issues"
-license: "INRIA Non-Commercial License Agreement"
-version: "3.7"
-build: [
-  ["./configure" "amd64-linux" {os = "linux"}
-  "amd64-macosx" {os = "macos"}
-  "amd64-cygwin" {os = "cygwin"}
-  "-prefix" "%{prefix}%/variants/compcert64"
-  "-install-coqdev"
-  "-clightgen"
-  "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert"
-  "-ignore-coq-version"]
-  [make "-j%{jobs}%" {ocaml:version >= "4.06"}]
-]
-patches: [
-  "0001-Install-compcert.config-file-along-the-Coq-developme.patch"
-  "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch"
-  "0008-Update-the-list-of-dual-licensed-files.patch"
-  "0011-Use-Coq-platform-supplied-Flocq.patch"
-  "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch"
-]
-extra-files: [
-  ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"]
-  ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"]
-  ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"]
-  ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"]
-  ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"]
-]
-install: [
-  [make "install"]
-]
-depends: [
-  "coq" {>= "8.7.0" & < "8.12"}
-  "coq-flocq" {>= "3.2.1"}
-  "coq-menhirlib" {>= "20190626" & < "20200123"}
-  "menhir" {>= "20190626" & < "20200123"}
-  "ocaml" {>= "4.05.0"}
-]
-synopsis: "The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)"
-description: "This package installs the 64 bit version of CompCert.
-For coexistence with the 32 bit version, the files are installed in:
-%{prefix}%/variants/compcert64/bin  (ccomp and clightgen binaries)
-%{prefix}%/variants/compcert64/lib/compcert  (C library)
-%{lib}%/coq/user-contrib/compcert64  (Coq library)
-Please note that the coq module path is compcert and not compcert64,
-so the files cannot be directly Required as compcert64.
-Instead -Q or -R options must be used to bind the compcert64 folder
-to the module path compcert. This is more convenient if one development
-uses both 32 and 64 bit versions. Otherwise all files would have to
-be duplicated with module paths compcert and compcert64.
-Please also note that the binary folder is usually not in the path."
-tags: [
-  "category:CS/Semantics and Compilation/Compilation"
-  "category:CS/Semantics and Compilation/Semantics"
-  "keyword:C"
-  "keyword:compiler"
-  "logpath:compcert64"
-  "date:2020-04-29"
-]
-url {
-  src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz"
-  checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0"
-}
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
deleted file mode 100644
index d160e66e23..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0001-Install-compcert.config-file-along-the-Coq-developme.patch
+++ /dev/null
@@ -1,82 +0,0 @@
-From cc465218dc80d4e7325622e9186c88e6a6ecdb12 Mon Sep 17 00:00:00 2001
-From: Xavier Leroy <xavier.leroy@college-de-france.fr>
-Date: Wed, 29 Apr 2020 15:40:13 +0200
-Subject: [PATCH 01/12] Install "compcert.config" file along the Coq
- development
-
-The file contains various parameters about the target processor and ABI,
-useful for VST and possibly other users of CompCert as a Coq library.
-
-It is in "var=val" syntax so that it can be included directly from
-a Makefile or a shell script.
----
- .gitignore |  1 +
- Makefile   | 19 ++++++++++++++++++-
- 2 files changed, 19 insertions(+), 1 deletion(-)
-
-diff --git a/.gitignore b/.gitignore
-index 6c10e1c3..b75ea5e7 100644
---- a/.gitignore
-+++ b/.gitignore
-@@ -31,6 +31,7 @@
- /.depend
- /.depend.extr
- /compcert.ini
-+/compcert.config
- /x86/ConstpropOp.v
- /x86/SelectOp.v
- /x86/SelectLong.v
-diff --git a/Makefile b/Makefile
-index aed0da28..df5fb03f 100644
---- a/Makefile
-+++ b/Makefile
-@@ -147,6 +147,9 @@ endif
- ifeq ($(CLIGHTGEN),true)
- 	$(MAKE) clightgen
- endif
-+ifeq ($(INSTALL_COQDEV),true)
-+	$(MAKE) compcert.config
-+endif
- 
- proof: $(FILES:.v=.vo)
- 
-@@ -224,6 +227,19 @@ compcert.ini: Makefile.config
- 	 echo "response_file_style=$(RESPONSEFILE)";) \
-         > compcert.ini
- 
-+compcert.config: Makefile.config
-+	(echo "# CompCert configuration parameters"; \
-+        echo "COMPCERT_ARCH=$(ARCH)"; \
-+        echo "COMPCERT_MODEL=$(MODEL)"; \
-+        echo "COMPCERT_ABI=$(ABI)"; \
-+        echo "COMPCERT_ENDIANNESS=$(ENDIANNESS)"; \
-+        echo "COMPCERT_BITSIZE=$(BITSIZE)"; \
-+        echo "COMPCERT_SYSTEM=$(SYSTEM)"; \
-+        echo "COMPCERT_VERSION=$(BUILDVERSION)"; \
-+        echo "COMPCERT_BUILDNR=$(BUILDNR)"; \
-+        echo "COMPCERT_TAG=$(TAG)" \
-+        ) > compcert.config
-+
- driver/Version.ml: VERSION
- 	(echo 'let version = "$(BUILDVERSION)"'; \
-          echo 'let buildnr = "$(BUILDNR)"'; \
-@@ -258,6 +274,7 @@ ifeq ($(INSTALL_COQDEV),true)
-           install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
- 	done
- 	install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
-+	install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
- 	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
- endif
- 
-@@ -267,7 +284,7 @@ clean:
- 	rm -f $(patsubst %, %/.*.aux, $(DIRS))
- 	rm -rf doc/html doc/*.glob
- 	rm -f driver/Version.ml
--	rm -f compcert.ini
-+	rm -f compcert.ini compcert.config
- 	rm -f extraction/STAMP extraction/*.ml extraction/*.mli .depend.extr
- 	rm -f tools/ndfun tools/modorder tools/*.cm? tools/*.o
- 	rm -f $(GENERATED) .depend
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
deleted file mode 100644
index f74202a53c..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch
+++ /dev/null
@@ -1,60 +0,0 @@
-From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001
-From: Xavier Leroy <xavier.leroy@college-de-france.fr>
-Date: Sun, 3 May 2020 09:43:14 +0200
-Subject: [PATCH 07/12] Dual-license
- aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}
-
-The corresponding files in all other ports are dual-licensed
-(GPL + non-commercial), there is no reason it should be different for
-aarch64.
----
- aarch64/Archi.v             | 3 +++
- aarch64/CBuiltins.ml        | 3 +++
- aarch64/extractionMachdep.v | 3 +++
- 3 files changed, 9 insertions(+)
-
-diff --git a/aarch64/Archi.v b/aarch64/Archi.v
-index aef4ab77..24431cb2 100644
---- a/aarch64/Archi.v
-+++ b/aarch64/Archi.v
-@@ -6,6 +6,9 @@
- (*                                                                     *)
- (*  Copyright Institut National de Recherche en Informatique et en     *)
- (*  Automatique.  All rights reserved.  This file is distributed       *)
-+(*  under the terms of the GNU General Public License as published by  *)
-+(*  the Free Software Foundation, either version 2 of the License, or  *)
-+(*  (at your option) any later version.  This file is also distributed *)
- (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
- (*                                                                     *)
- (* *********************************************************************)
-diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml
-index fdc1372d..dfd5b768 100644
---- a/aarch64/CBuiltins.ml
-+++ b/aarch64/CBuiltins.ml
-@@ -6,6 +6,9 @@
- (*                                                                     *)
- (*  Copyright Institut National de Recherche en Informatique et en     *)
- (*  Automatique.  All rights reserved.  This file is distributed       *)
-+(*  under the terms of the GNU General Public License as published by  *)
-+(*  the Free Software Foundation, either version 2 of the License, or  *)
-+(*  (at your option) any later version.  This file is also distributed *)
- (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
- (*                                                                     *)
- (* *********************************************************************)
-diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
-index e82056e2..5f26dc28 100644
---- a/aarch64/extractionMachdep.v
-+++ b/aarch64/extractionMachdep.v
-@@ -6,6 +6,9 @@
- (*                                                                     *)
- (*  Copyright Institut National de Recherche en Informatique et en     *)
- (*  Automatique.  All rights reserved.  This file is distributed       *)
-+(*  under the terms of the GNU General Public License as published by  *)
-+(*  the Free Software Foundation, either version 2 of the License, or  *)
-+(*  (at your option) any later version.  This file is also distributed *)
- (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
- (*                                                                     *)
- (* *********************************************************************)
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch
deleted file mode 100644
index 57bef5e519..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0008-Update-the-list-of-dual-licensed-files.patch
+++ /dev/null
@@ -1,28 +0,0 @@
-From b46c0c01379da17dd96fc0cb8f0458100b7b1e5e Mon Sep 17 00:00:00 2001
-From: Xavier Leroy <xavier.leroy@college-de-france.fr>
-Date: Mon, 4 May 2020 10:51:47 +0200
-Subject: [PATCH 08/12] Update the list of dual-licensed files
-
-Closes: #351
----
- LICENSE | 4 ++--
- 1 file changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/LICENSE b/LICENSE
-index 5a7ae79f..61b84219 100644
---- a/LICENSE
-+++ b/LICENSE
-@@ -46,8 +46,8 @@ option) any later version:
- 
-   all files in the exportclight/ directory
- 
--  the Archi.v, CBuiltins.ml, and extractionMachdep.v files
--  in directories arm, powerpc, riscV, x86, x86_32, x86_64
-+  the Archi.v, Builtins1.v, CBuiltins.ml, and extractionMachdep.v files
-+  in directories aarch64, arm, powerpc, riscV, x86, x86_32, x86_64
- 
-   extraction/extraction.v
- 
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch
deleted file mode 100644
index 28dbd06878..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0010-Added-open-source-build-to-makefile.patch
+++ /dev/null
@@ -1,106 +0,0 @@
-From b55c97d7930caec06d559faae4684761f258fd0f Mon Sep 17 00:00:00 2001
-From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
-Date: Thu, 30 Apr 2020 13:50:08 +0200
-Subject: [PATCH 10/12] Added open source build to makefile
-
----
- Makefile | 36 +++++++++++++++++++++++++++++++++---
- 1 file changed, 33 insertions(+), 3 deletions(-)
-
-diff --git a/Makefile b/Makefile
-index df5fb03f..48770ebd 100644
---- a/Makefile
-+++ b/Makefile
-@@ -57,10 +57,14 @@ FLOCQ=\
-   Relative.v Sterbenz.v Round_odd.v Double_rounding.v \
-   Binary.v Bits.v
- 
-+# Architecture files (in respective architecture folder)
-+
-+ARCHFILES=Archi.v
-+
- # General-purpose libraries (in lib/)
- 
- VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
--  Iteration.v Zbits.v Integers.v Archi.v IEEE754_extra.v Floats.v \
-+  Iteration.v Zbits.v Integers.v IEEE754_extra.v Floats.v \
-   Parmov.v UnionFind.v Wfsimpl.v \
-   Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v
- 
-@@ -101,6 +105,8 @@ BACKEND=\
-   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
-   Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
- 
-+BACKEND_OPEN_SOURCE=Cminor.v
-+  
- # C front-end modules (in cfrontend/)
- 
- CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \
-@@ -110,6 +116,8 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \
-   Cshmgen.v Cshmgenproof.v \
-   Csharpminor.v Cminorgen.v Cminorgenproof.v
- 
-+CFRONTEND_OPEN_SOURCE=Clight.v ClightBigstep.v Cop.v Csem.v Cstrategy.v Csyntax.v Ctypes.v Ctyping.v
-+
- # Parser
- 
- PARSER=Cabs.v Parser.v
-@@ -126,9 +134,17 @@ DRIVER=Compopts.v Compiler.v Complements.v
- 
- # All source files
- 
--FILES=$(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
-+FILES=$(ARCHFILES) $(VLIB) $(COMMON) $(BACKEND) $(CFRONTEND) $(DRIVER) $(FLOCQ) \
-   $(MENHIRLIB) $(PARSER)
- 
-+# All open source source files (in the order given in LICENSE)
-+
-+# ATTENTION: this also includes ./x86/Builtins1.vo - which is not open source but many files depend on it
-+
-+FILES_OPEN_SOURCE=$(VLIB) $(COMMON) $(CFRONTEND_OPEN_SOURCE) $(BACKEND_OPEN_SOURCE) $(PARSER) Clightdefs.v $(ARCHFILES) 
-+
-+# These files have non open dependencies: extractionMachdep.v, extraction.v
-+
- # Generated source files
- 
- GENERATED=\
-@@ -153,6 +169,8 @@ endif
- 
- proof: $(FILES:.v=.vo)
- 
-+proof_open_source: $(FILES_OPEN_SOURCE:.v=.vo) compcert.config
-+
- # Turn off some warnings for compiling Flocq
- flocq/%.vo: COQCOPTS+=-w -compatibility-notation
- 
-@@ -181,7 +199,7 @@ runtime:
- 
- FORCE:
- 
--.PHONY: proof extraction runtime FORCE
-+.PHONY: proof proof_open_source extraction runtime FORCE
- 
- documentation: $(FILES)
- 	mkdir -p doc/html
-@@ -278,6 +296,18 @@ ifeq ($(INSTALL_COQDEV),true)
- 	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
- endif
- 
-+# ToDo: copy exactly the files in FILES_OPEN_SOURCE as soon as the issue with Builtins1 ins fixed
-+install_open_source:
-+ifeq ($(INSTALL_COQDEV),true)
-+	install -d $(DESTDIR)$(COQDEVDIR)
-+	for d in $(DIRS); do \
-+          install -d $(DESTDIR)$(COQDEVDIR)/$$d && \
-+          install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \
-+	done
-+	install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR)
-+	install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
-+	@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
-+endif
- 
- clean:
- 	rm -f $(patsubst %, %/*.vo*, $(DIRS))
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch
deleted file mode 100644
index 0dc512b457..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0011-Use-Coq-platform-supplied-Flocq.patch
+++ /dev/null
@@ -1,123 +0,0 @@
-From 05448adb7642b3c1189139cec18c914b116d5d40 Mon Sep 17 00:00:00 2001
-From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
-Date: Thu, 30 Apr 2020 16:25:19 +0200
-Subject: [PATCH 11/12] Use Coq platform supplied Flocq
-
----
- aarch64/Archi.v     | 2 +-
- arm/Archi.v         | 2 +-
- lib/Floats.v        | 2 +-
- lib/IEEE754_extra.v | 2 +-
- powerpc/Archi.v     | 2 +-
- riscV/Archi.v       | 2 +-
- x86_32/Archi.v      | 2 +-
- x86_64/Archi.v      | 2 +-
- 8 files changed, 8 insertions(+), 8 deletions(-)
-
-diff --git a/aarch64/Archi.v b/aarch64/Archi.v
-index 24431cb2..6c5655d8 100644
---- a/aarch64/Archi.v
-+++ b/aarch64/Archi.v
-@@ -16,7 +16,7 @@
- (** Architecture-dependent parameters for AArch64 *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := true.
-diff --git a/arm/Archi.v b/arm/Archi.v
-index 16d6c71d..9b4cc96a 100644
---- a/arm/Archi.v
-+++ b/arm/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for ARM *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := false.
-diff --git a/lib/Floats.v b/lib/Floats.v
-index 6a126c3f..25a55620 100644
---- a/lib/Floats.v
-+++ b/lib/Floats.v
-@@ -17,7 +17,7 @@
- (** Formalization of floating-point numbers, using the Flocq library. *)
- 
- Require Import Coqlib Zbits Integers.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits Core.
- Require Import IEEE754_extra.
- Require Import Program.
-diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
-index c23149be..d546c7d3 100644
---- a/lib/IEEE754_extra.v
-+++ b/lib/IEEE754_extra.v
-@@ -20,7 +20,7 @@
- Require Import Psatz.
- Require Import Bool.
- Require Import Eqdep_dec.
--(*From Flocq *)
-+From Flocq
- Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd.
- 
- Local Open Scope Z_scope.
-diff --git a/powerpc/Archi.v b/powerpc/Archi.v
-index 10f38391..5ada45f4 100644
---- a/powerpc/Archi.v
-+++ b/powerpc/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for PowerPC *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := false.
-diff --git a/riscV/Archi.v b/riscV/Archi.v
-index 61d129d0..4a929aac 100644
---- a/riscV/Archi.v
-+++ b/riscV/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for RISC-V *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Parameter ptr64 : bool.
-diff --git a/x86_32/Archi.v b/x86_32/Archi.v
-index e9d05c14..b5e4b638 100644
---- a/x86_32/Archi.v
-+++ b/x86_32/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for x86 in 32-bit mode *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := false.
-diff --git a/x86_64/Archi.v b/x86_64/Archi.v
-index 959d8dc1..59502b4a 100644
---- a/x86_64/Archi.v
-+++ b/x86_64/Archi.v
-@@ -17,7 +17,7 @@
- (** Architecture-dependent parameters for x86 in 64-bit mode *)
- 
- Require Import ZArith List.
--(*From Flocq*)
-+From Flocq
- Require Import Binary Bits.
- 
- Definition ptr64 := true.
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
deleted file mode 100644
index 58a641f077..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/files/0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch
+++ /dev/null
@@ -1,26 +0,0 @@
-From 40fdac14428ef787ec94c137baea11fcfec6cb36 Mon Sep 17 00:00:00 2001
-From: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
-Date: Tue, 5 May 2020 17:10:06 +0200
-Subject: [PATCH 12/12] Use platform supplied menhirlib as suggested by
- jhjourdan
-
----
- Makefile | 2 +-
- 1 file changed, 1 insertion(+), 1 deletion(-)
-
-diff --git a/Makefile b/Makefile
-index 48770ebd..c4130630 100644
---- a/Makefile
-+++ b/Makefile
-@@ -265,7 +265,7 @@ driver/Version.ml: VERSION
- 
- cparser/Parser.v: cparser/Parser.vy
- 	@rm -f $@
--	$(MENHIR) --coq --coq-lib-path compcert.MenhirLib --coq-no-version-check cparser/Parser.vy
-+	$(MENHIR) --coq cparser/Parser.vy
- 	@chmod a-w $@
- 
- depend: $(GENERATED) depend1
--- 
-2.24.2 (Apple Git-127)
-
diff --git a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam b/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam
deleted file mode 100644
index ceca70c58c..0000000000
--- a/opam-prerelease/packages/coq-compcert-64/coq-compcert-64.3.7~coq-platform~open-source/opam
+++ /dev/null
@@ -1,71 +0,0 @@
-opam-version: "2.0"
-authors: "Xavier Leroy <xavier.leroy@inria.fr>"
-maintainer: "Jacques-Henri Jourdan <jacques-Henri.jourdan@normalesup.org>"
-homepage: "http://compcert.inria.fr/"
-dev-repo: "git+https://github.com/AbsInt/CompCert.git"
-bug-reports: "https://github.com/AbsInt/CompCert/issues"
-license: "INRIA Non-Commercial License Agreement"
-version: "3.7"
-build: [
-  ["./configure" "amd64-linux" {os = "linux"}
-  "amd64-macosx" {os = "macos"}
-  "amd64-cygwin" {os = "cygwin"}
-  "-prefix" "%{prefix}%/variants/compcert64"
-  "-install-coqdev"
-  "-clightgen"
-  "-coqdevdir" "%{lib}%/coq-variant/compcert64/compcert"
-  "-ignore-coq-version"]
-  [make "depend"]
-  [make "-j%{jobs}%" {ocaml:version >= "4.06"} "proof_open_source"]
-]
-patches: [
-  "0001-Install-compcert.config-file-along-the-Coq-developme.patch"
-  "0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch"
-  "0008-Update-the-list-of-dual-licensed-files.patch"
-  "0010-Added-open-source-build-to-makefile.patch"
-  "0011-Use-Coq-platform-supplied-Flocq.patch"
-  "0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch"
-]
-extra-files: [
-  ["0001-Install-compcert.config-file-along-the-Coq-developme.patch" "sha256=32ba8c21c84ae6a2075ecb0a039f05150e87db40728e64a81ea8d5daba6df541"]
-  ["0007-Dual-license-aarch64-Archi.v-Cbuiltins.ml-extraction.patch" "sha256=fd66f444b4097e4f20f53df9439ea5c66eb889183d271f6c1d45ce25793094d7"]
-  ["0008-Update-the-list-of-dual-licensed-files.patch" "sha256=406d241f0e9eb31d02a4be6ec5700044000a176ffe6cfeccf1ca52b42bdedb7d"]
-  ["0010-Added-open-source-build-to-makefile.patch" "sha256=fc3b8c1e097b53f209e7cf2e9b2e822609e8370857dbf1a4b34d909c37dcdfb5"]
-  ["0011-Use-Coq-platform-supplied-Flocq.patch" "sha256=1fd53e11083ca566e30b810acc68fc93d4fd5b5c55c2d493a86e0691c50fdff0"]
-  ["0012-Use-platform-supplied-menhirlib-as-suggested-by-jhjo.patch" "sha256=854f1ebbfed8829063f59c26c6e37dc164f98ecf60a572db0531a0d1f56b0981"]
-]
-install: [
-  [make "install_open_source"]
-]
-depends: [
-  "coq" {>= "8.7.0" & < "8.12"}
-  "coq-flocq" {>= "3.2.1"}
-  "coq-menhirlib" {>= "20190626" & < "20200123"}
-  "menhir" {>= "20190626" & < "20200123"}
-  "ocaml" {>= "4.05.0"}
-]
-synopsis: "The CompCert C compiler (64 bit, only open source files + using coq-platform)"
-description: "This package installs the 64 bit version of CompCert.
-For coexistence with the 32 bit version, the files are installed in:
-%{prefix}%/variants/compcert64/bin  (ccomp and clightgen binaries)
-%{prefix}%/variants/compcert64/lib/compcert  (C library)
-%{lib}%/coq/user-contrib/compcert64  (Coq library)
-Please note that the coq module path is compcert and not compcert64,
-so the files cannot be directly Required as compcert64.
-Instead -Q or -R options must be used to bind the compcert64 folder
-to the module path compcert. This is more convenient if one development
-uses both 32 and 64 bit versions. Otherwise all files would have to
-be duplicated with module paths compcert and compcert64.
-Please also note that the binary folder is usually not in the path."
-tags: [
-  "category:CS/Semantics and Compilation/Compilation"
-  "category:CS/Semantics and Compilation/Semantics"
-  "keyword:C"
-  "keyword:compiler"
-  "logpath:compcert64"
-  "date:2020-04-29"
-]
-url {
-  src: "https://github.com/AbsInt/CompCert/archive/v3.7.tar.gz"
-  checksum: "sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0"
-}