From 9ab29d8bf2e0d87cf6947b76ef96236d3633bb08 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 24 Jul 2026 15:41:20 +0200 Subject: [PATCH] coqPackages: move remaining derivations to rocq-modules --- .../CakeMLExtraction/default.nix | 0 .../CertiRocq/default.nix | 0 .../Cheerios/default.nix | 0 .../CoLoR/default.nix | 0 .../ConCert/default.nix | 0 .../ElmExtraction/default.nix | 0 .../ExtLib/default.nix | 0 .../HoTT/default.nix | 0 .../ITree/default.nix | 0 .../InfSeqExt/default.nix | 0 .../LibHyps/default.nix | 0 .../MenhirLib/default.nix | 0 .../Ordinal/default.nix | 0 .../QuickChick/default.nix | 0 .../RustExtraction/default.nix | 0 .../StructTact/default.nix | 0 .../TypedExtraction/default.nix | 0 .../VST/default.nix | 0 .../Velisarios/default.nix | 0 .../Verdi/default.nix | 0 .../Vpl/default.nix | 0 .../VplTactic/default.nix | 0 .../aac-tactics/default.nix | 0 .../addition-chains/default.nix | 0 .../async-test/default.nix | 0 .../atbr/default.nix | 0 .../autosubst-ocaml/default.nix | 0 .../autosubst/default.nix | 0 .../bbv/default.nix | 0 .../category-theory/default.nix | 0 .../ceres-bs/default.nix | 0 .../ceres/default.nix | 0 .../coinduction/default.nix | 0 .../compcert/default.nix | 0 .../contribs/default.nix | 0 .../coq-bits/default.nix | 0 .../coq-elpi/default.nix | 0 .../coq-hammer/default.nix | 0 .../coq-hammer/tactics.nix | 0 .../coq-haskell/default.nix | 0 .../coq-lsp/coq-loader.patch | 0 .../coq-lsp/default.nix | 0 .../coq-matrix/default.nix | 0 .../coq-record-update/default.nix | 0 .../coq-tactical/default.nix | 0 .../coqeal/default.nix | 0 .../coqfmt/default.nix | 0 .../coqhammer/default.nix | 0 .../coqide/default.nix | 0 .../coqprime/default.nix | 0 .../coqtail-math/default.nix | 0 .../coquelicot/default.nix | 0 .../coqutil/default.nix | 0 .../corn/default.nix | 0 .../deriving/default.nix | 0 .../dpdgraph/default.nix | 0 .../equations/default.nix | 0 .../extructures/default.nix | 0 .../fcsl-pcm/default.nix | 0 .../flocq/default.nix | 0 .../fourcolor/default.nix | 0 .../gaia-hydras/default.nix | 0 .../gaia/default.nix | 0 .../gappalib/default.nix | 0 .../goedel/default.nix | 0 .../graph-theory/default.nix | 0 .../heq/default.nix | 0 .../high-school-geometry/default.nix | 0 .../http/default.nix | 0 .../hydra-battles/default.nix | 0 .../interval/default.nix | 0 .../iris-named-props/default.nix | 0 .../itauto/default.nix | 0 .../itauto/test.nix | 0 .../itree-io/default.nix | 0 .../jasmin/default.nix | 0 .../json/default.nix | 0 .../lemma-overloading/default.nix | 0 .../ltac2/default.nix | 0 .../math-classes/default.nix | 0 .../mathcomp-abel/default.nix | 0 .../mathcomp-algebra-tactics/default.nix | 0 .../mathcomp-apery/default.nix | 0 .../mathcomp-infotheo/default.nix | 0 .../mathcomp-tarjan/default.nix | 0 .../mathcomp-word/default.nix | 0 .../mathcomp-zify/default.nix | 0 .../metacoq/default.nix | 0 .../metalib/default.nix | 0 .../metarocq/default.nix | 0 .../mtac2/default.nix | 0 .../multinomials/default.nix | 0 .../odd-order/default.nix | 0 .../paco/default.nix | 0 .../paramcoq/default.nix | 0 .../parsec/default.nix | 0 .../pocklington/default.nix | 0 .../reglang/default.nix | 0 .../rewriter/default.nix | 0 .../semantics/default.nix | 0 .../serapi/8.10.0+0.7.2.patch | 0 .../serapi/8.11.0+0.11.1.patch | 0 .../serapi/8.12.0+0.12.1.patch | 0 .../serapi/default.nix | 0 .../serapi/janestreet-0.15.patch | 0 .../serapi/janestreet-0.16.patch | 0 .../serapi/sertop.patch | 0 .../simple-io/default.nix | 0 .../simple-io/test.nix | 0 .../smpl/default.nix | 0 .../smtcoq/default.nix | 0 .../ssprove/default.nix | 0 .../stalmarck/default.nix | 0 .../tlc/default.nix | 0 .../topology/default.nix | 0 .../trakt/default.nix | 0 .../unicoq/default.nix | 0 .../validsdp/default.nix | 0 .../vcfloat/default.nix | 0 .../verified-extraction/default.nix | 0 .../vscoq-language-server/default.nix | 0 .../wasmcert/default.nix | 0 .../wasmcert/test.nix | 0 .../waterproof/default.nix | 0 .../zorns-lemma/default.nix | 0 pkgs/top-level/coq-packages.nix | 232 +++++++++--------- 126 files changed, 116 insertions(+), 116 deletions(-) rename pkgs/development/{coq-modules => rocq-modules}/CakeMLExtraction/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/CertiRocq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/Cheerios/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/CoLoR/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ConCert/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ElmExtraction/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ExtLib/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/HoTT/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ITree/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/InfSeqExt/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/LibHyps/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/MenhirLib/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/Ordinal/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/QuickChick/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/RustExtraction/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/StructTact/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/TypedExtraction/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/VST/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/Velisarios/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/Verdi/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/Vpl/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/VplTactic/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/aac-tactics/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/addition-chains/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/async-test/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/atbr/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/autosubst-ocaml/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/autosubst/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/bbv/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/category-theory/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ceres-bs/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ceres/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coinduction/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/compcert/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/contribs/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-bits/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-elpi/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-hammer/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-hammer/tactics.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-haskell/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-lsp/coq-loader.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-lsp/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-matrix/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-record-update/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coq-tactical/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqeal/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqfmt/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqhammer/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqide/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqprime/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqtail-math/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coquelicot/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/coqutil/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/corn/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/deriving/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/dpdgraph/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/equations/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/extructures/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/fcsl-pcm/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/flocq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/fourcolor/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/gaia-hydras/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/gaia/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/gappalib/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/goedel/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/graph-theory/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/heq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/high-school-geometry/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/http/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/hydra-battles/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/interval/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/iris-named-props/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/itauto/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/itauto/test.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/itree-io/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/jasmin/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/json/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/lemma-overloading/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ltac2/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/math-classes/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-abel/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-algebra-tactics/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-apery/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-infotheo/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-tarjan/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-word/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mathcomp-zify/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/metacoq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/metalib/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/metarocq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/mtac2/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/multinomials/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/odd-order/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/paco/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/paramcoq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/parsec/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/pocklington/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/reglang/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/rewriter/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/semantics/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/8.10.0+0.7.2.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/8.11.0+0.11.1.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/8.12.0+0.12.1.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/janestreet-0.15.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/janestreet-0.16.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/serapi/sertop.patch (100%) rename pkgs/development/{coq-modules => rocq-modules}/simple-io/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/simple-io/test.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/smpl/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/smtcoq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/ssprove/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/stalmarck/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/tlc/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/topology/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/trakt/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/unicoq/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/validsdp/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/vcfloat/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/verified-extraction/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/vscoq-language-server/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/wasmcert/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/wasmcert/test.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/waterproof/default.nix (100%) rename pkgs/development/{coq-modules => rocq-modules}/zorns-lemma/default.nix (100%) diff --git a/pkgs/development/coq-modules/CakeMLExtraction/default.nix b/pkgs/development/rocq-modules/CakeMLExtraction/default.nix similarity index 100% rename from pkgs/development/coq-modules/CakeMLExtraction/default.nix rename to pkgs/development/rocq-modules/CakeMLExtraction/default.nix diff --git a/pkgs/development/coq-modules/CertiRocq/default.nix b/pkgs/development/rocq-modules/CertiRocq/default.nix similarity index 100% rename from pkgs/development/coq-modules/CertiRocq/default.nix rename to pkgs/development/rocq-modules/CertiRocq/default.nix diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/rocq-modules/Cheerios/default.nix similarity index 100% rename from pkgs/development/coq-modules/Cheerios/default.nix rename to pkgs/development/rocq-modules/Cheerios/default.nix diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/rocq-modules/CoLoR/default.nix similarity index 100% rename from pkgs/development/coq-modules/CoLoR/default.nix rename to pkgs/development/rocq-modules/CoLoR/default.nix diff --git a/pkgs/development/coq-modules/ConCert/default.nix b/pkgs/development/rocq-modules/ConCert/default.nix similarity index 100% rename from pkgs/development/coq-modules/ConCert/default.nix rename to pkgs/development/rocq-modules/ConCert/default.nix diff --git a/pkgs/development/coq-modules/ElmExtraction/default.nix b/pkgs/development/rocq-modules/ElmExtraction/default.nix similarity index 100% rename from pkgs/development/coq-modules/ElmExtraction/default.nix rename to pkgs/development/rocq-modules/ElmExtraction/default.nix diff --git a/pkgs/development/coq-modules/ExtLib/default.nix b/pkgs/development/rocq-modules/ExtLib/default.nix similarity index 100% rename from pkgs/development/coq-modules/ExtLib/default.nix rename to pkgs/development/rocq-modules/ExtLib/default.nix diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/rocq-modules/HoTT/default.nix similarity index 100% rename from pkgs/development/coq-modules/HoTT/default.nix rename to pkgs/development/rocq-modules/HoTT/default.nix diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/rocq-modules/ITree/default.nix similarity index 100% rename from pkgs/development/coq-modules/ITree/default.nix rename to pkgs/development/rocq-modules/ITree/default.nix diff --git a/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/rocq-modules/InfSeqExt/default.nix similarity index 100% rename from pkgs/development/coq-modules/InfSeqExt/default.nix rename to pkgs/development/rocq-modules/InfSeqExt/default.nix diff --git a/pkgs/development/coq-modules/LibHyps/default.nix b/pkgs/development/rocq-modules/LibHyps/default.nix similarity index 100% rename from pkgs/development/coq-modules/LibHyps/default.nix rename to pkgs/development/rocq-modules/LibHyps/default.nix diff --git a/pkgs/development/coq-modules/MenhirLib/default.nix b/pkgs/development/rocq-modules/MenhirLib/default.nix similarity index 100% rename from pkgs/development/coq-modules/MenhirLib/default.nix rename to pkgs/development/rocq-modules/MenhirLib/default.nix diff --git a/pkgs/development/coq-modules/Ordinal/default.nix b/pkgs/development/rocq-modules/Ordinal/default.nix similarity index 100% rename from pkgs/development/coq-modules/Ordinal/default.nix rename to pkgs/development/rocq-modules/Ordinal/default.nix diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/rocq-modules/QuickChick/default.nix similarity index 100% rename from pkgs/development/coq-modules/QuickChick/default.nix rename to pkgs/development/rocq-modules/QuickChick/default.nix diff --git a/pkgs/development/coq-modules/RustExtraction/default.nix b/pkgs/development/rocq-modules/RustExtraction/default.nix similarity index 100% rename from pkgs/development/coq-modules/RustExtraction/default.nix rename to pkgs/development/rocq-modules/RustExtraction/default.nix diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/rocq-modules/StructTact/default.nix similarity index 100% rename from pkgs/development/coq-modules/StructTact/default.nix rename to pkgs/development/rocq-modules/StructTact/default.nix diff --git a/pkgs/development/coq-modules/TypedExtraction/default.nix b/pkgs/development/rocq-modules/TypedExtraction/default.nix similarity index 100% rename from pkgs/development/coq-modules/TypedExtraction/default.nix rename to pkgs/development/rocq-modules/TypedExtraction/default.nix diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/rocq-modules/VST/default.nix similarity index 100% rename from pkgs/development/coq-modules/VST/default.nix rename to pkgs/development/rocq-modules/VST/default.nix diff --git a/pkgs/development/coq-modules/Velisarios/default.nix b/pkgs/development/rocq-modules/Velisarios/default.nix similarity index 100% rename from pkgs/development/coq-modules/Velisarios/default.nix rename to pkgs/development/rocq-modules/Velisarios/default.nix diff --git a/pkgs/development/coq-modules/Verdi/default.nix b/pkgs/development/rocq-modules/Verdi/default.nix similarity index 100% rename from pkgs/development/coq-modules/Verdi/default.nix rename to pkgs/development/rocq-modules/Verdi/default.nix diff --git a/pkgs/development/coq-modules/Vpl/default.nix b/pkgs/development/rocq-modules/Vpl/default.nix similarity index 100% rename from pkgs/development/coq-modules/Vpl/default.nix rename to pkgs/development/rocq-modules/Vpl/default.nix diff --git a/pkgs/development/coq-modules/VplTactic/default.nix b/pkgs/development/rocq-modules/VplTactic/default.nix similarity index 100% rename from pkgs/development/coq-modules/VplTactic/default.nix rename to pkgs/development/rocq-modules/VplTactic/default.nix diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/rocq-modules/aac-tactics/default.nix similarity index 100% rename from pkgs/development/coq-modules/aac-tactics/default.nix rename to pkgs/development/rocq-modules/aac-tactics/default.nix diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/rocq-modules/addition-chains/default.nix similarity index 100% rename from pkgs/development/coq-modules/addition-chains/default.nix rename to pkgs/development/rocq-modules/addition-chains/default.nix diff --git a/pkgs/development/coq-modules/async-test/default.nix b/pkgs/development/rocq-modules/async-test/default.nix similarity index 100% rename from pkgs/development/coq-modules/async-test/default.nix rename to pkgs/development/rocq-modules/async-test/default.nix diff --git a/pkgs/development/coq-modules/atbr/default.nix b/pkgs/development/rocq-modules/atbr/default.nix similarity index 100% rename from pkgs/development/coq-modules/atbr/default.nix rename to pkgs/development/rocq-modules/atbr/default.nix diff --git a/pkgs/development/coq-modules/autosubst-ocaml/default.nix b/pkgs/development/rocq-modules/autosubst-ocaml/default.nix similarity index 100% rename from pkgs/development/coq-modules/autosubst-ocaml/default.nix rename to pkgs/development/rocq-modules/autosubst-ocaml/default.nix diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/rocq-modules/autosubst/default.nix similarity index 100% rename from pkgs/development/coq-modules/autosubst/default.nix rename to pkgs/development/rocq-modules/autosubst/default.nix diff --git a/pkgs/development/coq-modules/bbv/default.nix b/pkgs/development/rocq-modules/bbv/default.nix similarity index 100% rename from pkgs/development/coq-modules/bbv/default.nix rename to pkgs/development/rocq-modules/bbv/default.nix diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/rocq-modules/category-theory/default.nix similarity index 100% rename from pkgs/development/coq-modules/category-theory/default.nix rename to pkgs/development/rocq-modules/category-theory/default.nix diff --git a/pkgs/development/coq-modules/ceres-bs/default.nix b/pkgs/development/rocq-modules/ceres-bs/default.nix similarity index 100% rename from pkgs/development/coq-modules/ceres-bs/default.nix rename to pkgs/development/rocq-modules/ceres-bs/default.nix diff --git a/pkgs/development/coq-modules/ceres/default.nix b/pkgs/development/rocq-modules/ceres/default.nix similarity index 100% rename from pkgs/development/coq-modules/ceres/default.nix rename to pkgs/development/rocq-modules/ceres/default.nix diff --git a/pkgs/development/coq-modules/coinduction/default.nix b/pkgs/development/rocq-modules/coinduction/default.nix similarity index 100% rename from pkgs/development/coq-modules/coinduction/default.nix rename to pkgs/development/rocq-modules/coinduction/default.nix diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/rocq-modules/compcert/default.nix similarity index 100% rename from pkgs/development/coq-modules/compcert/default.nix rename to pkgs/development/rocq-modules/compcert/default.nix diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/rocq-modules/contribs/default.nix similarity index 100% rename from pkgs/development/coq-modules/contribs/default.nix rename to pkgs/development/rocq-modules/contribs/default.nix diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/rocq-modules/coq-bits/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-bits/default.nix rename to pkgs/development/rocq-modules/coq-bits/default.nix diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/rocq-modules/coq-elpi/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-elpi/default.nix rename to pkgs/development/rocq-modules/coq-elpi/default.nix diff --git a/pkgs/development/coq-modules/coq-hammer/default.nix b/pkgs/development/rocq-modules/coq-hammer/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-hammer/default.nix rename to pkgs/development/rocq-modules/coq-hammer/default.nix diff --git a/pkgs/development/coq-modules/coq-hammer/tactics.nix b/pkgs/development/rocq-modules/coq-hammer/tactics.nix similarity index 100% rename from pkgs/development/coq-modules/coq-hammer/tactics.nix rename to pkgs/development/rocq-modules/coq-hammer/tactics.nix diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/rocq-modules/coq-haskell/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-haskell/default.nix rename to pkgs/development/rocq-modules/coq-haskell/default.nix diff --git a/pkgs/development/coq-modules/coq-lsp/coq-loader.patch b/pkgs/development/rocq-modules/coq-lsp/coq-loader.patch similarity index 100% rename from pkgs/development/coq-modules/coq-lsp/coq-loader.patch rename to pkgs/development/rocq-modules/coq-lsp/coq-loader.patch diff --git a/pkgs/development/coq-modules/coq-lsp/default.nix b/pkgs/development/rocq-modules/coq-lsp/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-lsp/default.nix rename to pkgs/development/rocq-modules/coq-lsp/default.nix diff --git a/pkgs/development/coq-modules/coq-matrix/default.nix b/pkgs/development/rocq-modules/coq-matrix/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-matrix/default.nix rename to pkgs/development/rocq-modules/coq-matrix/default.nix diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/rocq-modules/coq-record-update/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-record-update/default.nix rename to pkgs/development/rocq-modules/coq-record-update/default.nix diff --git a/pkgs/development/coq-modules/coq-tactical/default.nix b/pkgs/development/rocq-modules/coq-tactical/default.nix similarity index 100% rename from pkgs/development/coq-modules/coq-tactical/default.nix rename to pkgs/development/rocq-modules/coq-tactical/default.nix diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/rocq-modules/coqeal/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqeal/default.nix rename to pkgs/development/rocq-modules/coqeal/default.nix diff --git a/pkgs/development/coq-modules/coqfmt/default.nix b/pkgs/development/rocq-modules/coqfmt/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqfmt/default.nix rename to pkgs/development/rocq-modules/coqfmt/default.nix diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/rocq-modules/coqhammer/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqhammer/default.nix rename to pkgs/development/rocq-modules/coqhammer/default.nix diff --git a/pkgs/development/coq-modules/coqide/default.nix b/pkgs/development/rocq-modules/coqide/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqide/default.nix rename to pkgs/development/rocq-modules/coqide/default.nix diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/rocq-modules/coqprime/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqprime/default.nix rename to pkgs/development/rocq-modules/coqprime/default.nix diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/rocq-modules/coqtail-math/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqtail-math/default.nix rename to pkgs/development/rocq-modules/coqtail-math/default.nix diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/rocq-modules/coquelicot/default.nix similarity index 100% rename from pkgs/development/coq-modules/coquelicot/default.nix rename to pkgs/development/rocq-modules/coquelicot/default.nix diff --git a/pkgs/development/coq-modules/coqutil/default.nix b/pkgs/development/rocq-modules/coqutil/default.nix similarity index 100% rename from pkgs/development/coq-modules/coqutil/default.nix rename to pkgs/development/rocq-modules/coqutil/default.nix diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/rocq-modules/corn/default.nix similarity index 100% rename from pkgs/development/coq-modules/corn/default.nix rename to pkgs/development/rocq-modules/corn/default.nix diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/rocq-modules/deriving/default.nix similarity index 100% rename from pkgs/development/coq-modules/deriving/default.nix rename to pkgs/development/rocq-modules/deriving/default.nix diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/rocq-modules/dpdgraph/default.nix similarity index 100% rename from pkgs/development/coq-modules/dpdgraph/default.nix rename to pkgs/development/rocq-modules/dpdgraph/default.nix diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/rocq-modules/equations/default.nix similarity index 100% rename from pkgs/development/coq-modules/equations/default.nix rename to pkgs/development/rocq-modules/equations/default.nix diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/rocq-modules/extructures/default.nix similarity index 100% rename from pkgs/development/coq-modules/extructures/default.nix rename to pkgs/development/rocq-modules/extructures/default.nix diff --git a/pkgs/development/coq-modules/fcsl-pcm/default.nix b/pkgs/development/rocq-modules/fcsl-pcm/default.nix similarity index 100% rename from pkgs/development/coq-modules/fcsl-pcm/default.nix rename to pkgs/development/rocq-modules/fcsl-pcm/default.nix diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/rocq-modules/flocq/default.nix similarity index 100% rename from pkgs/development/coq-modules/flocq/default.nix rename to pkgs/development/rocq-modules/flocq/default.nix diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/rocq-modules/fourcolor/default.nix similarity index 100% rename from pkgs/development/coq-modules/fourcolor/default.nix rename to pkgs/development/rocq-modules/fourcolor/default.nix diff --git a/pkgs/development/coq-modules/gaia-hydras/default.nix b/pkgs/development/rocq-modules/gaia-hydras/default.nix similarity index 100% rename from pkgs/development/coq-modules/gaia-hydras/default.nix rename to pkgs/development/rocq-modules/gaia-hydras/default.nix diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/rocq-modules/gaia/default.nix similarity index 100% rename from pkgs/development/coq-modules/gaia/default.nix rename to pkgs/development/rocq-modules/gaia/default.nix diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/rocq-modules/gappalib/default.nix similarity index 100% rename from pkgs/development/coq-modules/gappalib/default.nix rename to pkgs/development/rocq-modules/gappalib/default.nix diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/rocq-modules/goedel/default.nix similarity index 100% rename from pkgs/development/coq-modules/goedel/default.nix rename to pkgs/development/rocq-modules/goedel/default.nix diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/rocq-modules/graph-theory/default.nix similarity index 100% rename from pkgs/development/coq-modules/graph-theory/default.nix rename to pkgs/development/rocq-modules/graph-theory/default.nix diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/rocq-modules/heq/default.nix similarity index 100% rename from pkgs/development/coq-modules/heq/default.nix rename to pkgs/development/rocq-modules/heq/default.nix diff --git a/pkgs/development/coq-modules/high-school-geometry/default.nix b/pkgs/development/rocq-modules/high-school-geometry/default.nix similarity index 100% rename from pkgs/development/coq-modules/high-school-geometry/default.nix rename to pkgs/development/rocq-modules/high-school-geometry/default.nix diff --git a/pkgs/development/coq-modules/http/default.nix b/pkgs/development/rocq-modules/http/default.nix similarity index 100% rename from pkgs/development/coq-modules/http/default.nix rename to pkgs/development/rocq-modules/http/default.nix diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/rocq-modules/hydra-battles/default.nix similarity index 100% rename from pkgs/development/coq-modules/hydra-battles/default.nix rename to pkgs/development/rocq-modules/hydra-battles/default.nix diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/rocq-modules/interval/default.nix similarity index 100% rename from pkgs/development/coq-modules/interval/default.nix rename to pkgs/development/rocq-modules/interval/default.nix diff --git a/pkgs/development/coq-modules/iris-named-props/default.nix b/pkgs/development/rocq-modules/iris-named-props/default.nix similarity index 100% rename from pkgs/development/coq-modules/iris-named-props/default.nix rename to pkgs/development/rocq-modules/iris-named-props/default.nix diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/rocq-modules/itauto/default.nix similarity index 100% rename from pkgs/development/coq-modules/itauto/default.nix rename to pkgs/development/rocq-modules/itauto/default.nix diff --git a/pkgs/development/coq-modules/itauto/test.nix b/pkgs/development/rocq-modules/itauto/test.nix similarity index 100% rename from pkgs/development/coq-modules/itauto/test.nix rename to pkgs/development/rocq-modules/itauto/test.nix diff --git a/pkgs/development/coq-modules/itree-io/default.nix b/pkgs/development/rocq-modules/itree-io/default.nix similarity index 100% rename from pkgs/development/coq-modules/itree-io/default.nix rename to pkgs/development/rocq-modules/itree-io/default.nix diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/rocq-modules/jasmin/default.nix similarity index 100% rename from pkgs/development/coq-modules/jasmin/default.nix rename to pkgs/development/rocq-modules/jasmin/default.nix diff --git a/pkgs/development/coq-modules/json/default.nix b/pkgs/development/rocq-modules/json/default.nix similarity index 100% rename from pkgs/development/coq-modules/json/default.nix rename to pkgs/development/rocq-modules/json/default.nix diff --git a/pkgs/development/coq-modules/lemma-overloading/default.nix b/pkgs/development/rocq-modules/lemma-overloading/default.nix similarity index 100% rename from pkgs/development/coq-modules/lemma-overloading/default.nix rename to pkgs/development/rocq-modules/lemma-overloading/default.nix diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/rocq-modules/ltac2/default.nix similarity index 100% rename from pkgs/development/coq-modules/ltac2/default.nix rename to pkgs/development/rocq-modules/ltac2/default.nix diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/rocq-modules/math-classes/default.nix similarity index 100% rename from pkgs/development/coq-modules/math-classes/default.nix rename to pkgs/development/rocq-modules/math-classes/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/rocq-modules/mathcomp-abel/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-abel/default.nix rename to pkgs/development/rocq-modules/mathcomp-abel/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix b/pkgs/development/rocq-modules/mathcomp-algebra-tactics/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix rename to pkgs/development/rocq-modules/mathcomp-algebra-tactics/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/rocq-modules/mathcomp-apery/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-apery/default.nix rename to pkgs/development/rocq-modules/mathcomp-apery/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-infotheo/default.nix b/pkgs/development/rocq-modules/mathcomp-infotheo/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-infotheo/default.nix rename to pkgs/development/rocq-modules/mathcomp-infotheo/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/rocq-modules/mathcomp-tarjan/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-tarjan/default.nix rename to pkgs/development/rocq-modules/mathcomp-tarjan/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/rocq-modules/mathcomp-word/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-word/default.nix rename to pkgs/development/rocq-modules/mathcomp-word/default.nix diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/rocq-modules/mathcomp-zify/default.nix similarity index 100% rename from pkgs/development/coq-modules/mathcomp-zify/default.nix rename to pkgs/development/rocq-modules/mathcomp-zify/default.nix diff --git a/pkgs/development/coq-modules/metacoq/default.nix b/pkgs/development/rocq-modules/metacoq/default.nix similarity index 100% rename from pkgs/development/coq-modules/metacoq/default.nix rename to pkgs/development/rocq-modules/metacoq/default.nix diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/rocq-modules/metalib/default.nix similarity index 100% rename from pkgs/development/coq-modules/metalib/default.nix rename to pkgs/development/rocq-modules/metalib/default.nix diff --git a/pkgs/development/coq-modules/metarocq/default.nix b/pkgs/development/rocq-modules/metarocq/default.nix similarity index 100% rename from pkgs/development/coq-modules/metarocq/default.nix rename to pkgs/development/rocq-modules/metarocq/default.nix diff --git a/pkgs/development/coq-modules/mtac2/default.nix b/pkgs/development/rocq-modules/mtac2/default.nix similarity index 100% rename from pkgs/development/coq-modules/mtac2/default.nix rename to pkgs/development/rocq-modules/mtac2/default.nix diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/rocq-modules/multinomials/default.nix similarity index 100% rename from pkgs/development/coq-modules/multinomials/default.nix rename to pkgs/development/rocq-modules/multinomials/default.nix diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/rocq-modules/odd-order/default.nix similarity index 100% rename from pkgs/development/coq-modules/odd-order/default.nix rename to pkgs/development/rocq-modules/odd-order/default.nix diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/rocq-modules/paco/default.nix similarity index 100% rename from pkgs/development/coq-modules/paco/default.nix rename to pkgs/development/rocq-modules/paco/default.nix diff --git a/pkgs/development/coq-modules/paramcoq/default.nix b/pkgs/development/rocq-modules/paramcoq/default.nix similarity index 100% rename from pkgs/development/coq-modules/paramcoq/default.nix rename to pkgs/development/rocq-modules/paramcoq/default.nix diff --git a/pkgs/development/coq-modules/parsec/default.nix b/pkgs/development/rocq-modules/parsec/default.nix similarity index 100% rename from pkgs/development/coq-modules/parsec/default.nix rename to pkgs/development/rocq-modules/parsec/default.nix diff --git a/pkgs/development/coq-modules/pocklington/default.nix b/pkgs/development/rocq-modules/pocklington/default.nix similarity index 100% rename from pkgs/development/coq-modules/pocklington/default.nix rename to pkgs/development/rocq-modules/pocklington/default.nix diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/rocq-modules/reglang/default.nix similarity index 100% rename from pkgs/development/coq-modules/reglang/default.nix rename to pkgs/development/rocq-modules/reglang/default.nix diff --git a/pkgs/development/coq-modules/rewriter/default.nix b/pkgs/development/rocq-modules/rewriter/default.nix similarity index 100% rename from pkgs/development/coq-modules/rewriter/default.nix rename to pkgs/development/rocq-modules/rewriter/default.nix diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/rocq-modules/semantics/default.nix similarity index 100% rename from pkgs/development/coq-modules/semantics/default.nix rename to pkgs/development/rocq-modules/semantics/default.nix diff --git a/pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch b/pkgs/development/rocq-modules/serapi/8.10.0+0.7.2.patch similarity index 100% rename from pkgs/development/coq-modules/serapi/8.10.0+0.7.2.patch rename to pkgs/development/rocq-modules/serapi/8.10.0+0.7.2.patch diff --git a/pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch b/pkgs/development/rocq-modules/serapi/8.11.0+0.11.1.patch similarity index 100% rename from pkgs/development/coq-modules/serapi/8.11.0+0.11.1.patch rename to pkgs/development/rocq-modules/serapi/8.11.0+0.11.1.patch diff --git a/pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch b/pkgs/development/rocq-modules/serapi/8.12.0+0.12.1.patch similarity index 100% rename from pkgs/development/coq-modules/serapi/8.12.0+0.12.1.patch rename to pkgs/development/rocq-modules/serapi/8.12.0+0.12.1.patch diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/rocq-modules/serapi/default.nix similarity index 100% rename from pkgs/development/coq-modules/serapi/default.nix rename to pkgs/development/rocq-modules/serapi/default.nix diff --git a/pkgs/development/coq-modules/serapi/janestreet-0.15.patch b/pkgs/development/rocq-modules/serapi/janestreet-0.15.patch similarity index 100% rename from pkgs/development/coq-modules/serapi/janestreet-0.15.patch rename to pkgs/development/rocq-modules/serapi/janestreet-0.15.patch diff --git a/pkgs/development/coq-modules/serapi/janestreet-0.16.patch b/pkgs/development/rocq-modules/serapi/janestreet-0.16.patch similarity index 100% rename from pkgs/development/coq-modules/serapi/janestreet-0.16.patch rename to pkgs/development/rocq-modules/serapi/janestreet-0.16.patch diff --git a/pkgs/development/coq-modules/serapi/sertop.patch b/pkgs/development/rocq-modules/serapi/sertop.patch similarity index 100% rename from pkgs/development/coq-modules/serapi/sertop.patch rename to pkgs/development/rocq-modules/serapi/sertop.patch diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/rocq-modules/simple-io/default.nix similarity index 100% rename from pkgs/development/coq-modules/simple-io/default.nix rename to pkgs/development/rocq-modules/simple-io/default.nix diff --git a/pkgs/development/coq-modules/simple-io/test.nix b/pkgs/development/rocq-modules/simple-io/test.nix similarity index 100% rename from pkgs/development/coq-modules/simple-io/test.nix rename to pkgs/development/rocq-modules/simple-io/test.nix diff --git a/pkgs/development/coq-modules/smpl/default.nix b/pkgs/development/rocq-modules/smpl/default.nix similarity index 100% rename from pkgs/development/coq-modules/smpl/default.nix rename to pkgs/development/rocq-modules/smpl/default.nix diff --git a/pkgs/development/coq-modules/smtcoq/default.nix b/pkgs/development/rocq-modules/smtcoq/default.nix similarity index 100% rename from pkgs/development/coq-modules/smtcoq/default.nix rename to pkgs/development/rocq-modules/smtcoq/default.nix diff --git a/pkgs/development/coq-modules/ssprove/default.nix b/pkgs/development/rocq-modules/ssprove/default.nix similarity index 100% rename from pkgs/development/coq-modules/ssprove/default.nix rename to pkgs/development/rocq-modules/ssprove/default.nix diff --git a/pkgs/development/coq-modules/stalmarck/default.nix b/pkgs/development/rocq-modules/stalmarck/default.nix similarity index 100% rename from pkgs/development/coq-modules/stalmarck/default.nix rename to pkgs/development/rocq-modules/stalmarck/default.nix diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/rocq-modules/tlc/default.nix similarity index 100% rename from pkgs/development/coq-modules/tlc/default.nix rename to pkgs/development/rocq-modules/tlc/default.nix diff --git a/pkgs/development/coq-modules/topology/default.nix b/pkgs/development/rocq-modules/topology/default.nix similarity index 100% rename from pkgs/development/coq-modules/topology/default.nix rename to pkgs/development/rocq-modules/topology/default.nix diff --git a/pkgs/development/coq-modules/trakt/default.nix b/pkgs/development/rocq-modules/trakt/default.nix similarity index 100% rename from pkgs/development/coq-modules/trakt/default.nix rename to pkgs/development/rocq-modules/trakt/default.nix diff --git a/pkgs/development/coq-modules/unicoq/default.nix b/pkgs/development/rocq-modules/unicoq/default.nix similarity index 100% rename from pkgs/development/coq-modules/unicoq/default.nix rename to pkgs/development/rocq-modules/unicoq/default.nix diff --git a/pkgs/development/coq-modules/validsdp/default.nix b/pkgs/development/rocq-modules/validsdp/default.nix similarity index 100% rename from pkgs/development/coq-modules/validsdp/default.nix rename to pkgs/development/rocq-modules/validsdp/default.nix diff --git a/pkgs/development/coq-modules/vcfloat/default.nix b/pkgs/development/rocq-modules/vcfloat/default.nix similarity index 100% rename from pkgs/development/coq-modules/vcfloat/default.nix rename to pkgs/development/rocq-modules/vcfloat/default.nix diff --git a/pkgs/development/coq-modules/verified-extraction/default.nix b/pkgs/development/rocq-modules/verified-extraction/default.nix similarity index 100% rename from pkgs/development/coq-modules/verified-extraction/default.nix rename to pkgs/development/rocq-modules/verified-extraction/default.nix diff --git a/pkgs/development/coq-modules/vscoq-language-server/default.nix b/pkgs/development/rocq-modules/vscoq-language-server/default.nix similarity index 100% rename from pkgs/development/coq-modules/vscoq-language-server/default.nix rename to pkgs/development/rocq-modules/vscoq-language-server/default.nix diff --git a/pkgs/development/coq-modules/wasmcert/default.nix b/pkgs/development/rocq-modules/wasmcert/default.nix similarity index 100% rename from pkgs/development/coq-modules/wasmcert/default.nix rename to pkgs/development/rocq-modules/wasmcert/default.nix diff --git a/pkgs/development/coq-modules/wasmcert/test.nix b/pkgs/development/rocq-modules/wasmcert/test.nix similarity index 100% rename from pkgs/development/coq-modules/wasmcert/test.nix rename to pkgs/development/rocq-modules/wasmcert/test.nix diff --git a/pkgs/development/coq-modules/waterproof/default.nix b/pkgs/development/rocq-modules/waterproof/default.nix similarity index 100% rename from pkgs/development/coq-modules/waterproof/default.nix rename to pkgs/development/rocq-modules/waterproof/default.nix diff --git a/pkgs/development/coq-modules/zorns-lemma/default.nix b/pkgs/development/rocq-modules/zorns-lemma/default.nix similarity index 100% rename from pkgs/development/coq-modules/zorns-lemma/default.nix rename to pkgs/development/rocq-modules/zorns-lemma/default.nix diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 79bb123762b3..8273903e6696 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/pkgs/top-level/coq-packages.nix @@ -65,29 +65,29 @@ let }; }); - contribs = lib.recurseIntoAttrs (callPackage ../development/coq-modules/contribs { }); + contribs = lib.recurseIntoAttrs (callPackage ../development/rocq-modules/contribs { }); - aac-tactics = callPackage ../development/coq-modules/aac-tactics { }; - addition-chains = callPackage ../development/coq-modules/addition-chains { }; - async-test = callPackage ../development/coq-modules/async-test { }; - atbr = callPackage ../development/coq-modules/atbr { }; - autosubst = callPackage ../development/coq-modules/autosubst { }; - autosubst-ocaml = callPackage ../development/coq-modules/autosubst-ocaml { }; - bbv = callPackage ../development/coq-modules/bbv { }; + aac-tactics = callPackage ../development/rocq-modules/aac-tactics { }; + addition-chains = callPackage ../development/rocq-modules/addition-chains { }; + async-test = callPackage ../development/rocq-modules/async-test { }; + atbr = callPackage ../development/rocq-modules/atbr { }; + autosubst = callPackage ../development/rocq-modules/autosubst { }; + autosubst-ocaml = callPackage ../development/rocq-modules/autosubst-ocaml { }; + bbv = callPackage ../development/rocq-modules/bbv { }; bignums = callPackage ../development/rocq-modules/bignums { }; - CakeMLExtraction = callPackage ../development/coq-modules/CakeMLExtraction { }; - category-theory = callPackage ../development/coq-modules/category-theory { }; - ceres = callPackage ../development/coq-modules/ceres { }; - ceres-bs = callPackage ../development/coq-modules/ceres-bs { }; - CertiRocq = callPackage ../development/coq-modules/CertiRocq { }; - Cheerios = callPackage ../development/coq-modules/Cheerios { }; - coinduction = callPackage ../development/coq-modules/coinduction { }; - CoLoR = callPackage ../development/coq-modules/CoLoR ( + CakeMLExtraction = callPackage ../development/rocq-modules/CakeMLExtraction { }; + category-theory = callPackage ../development/rocq-modules/category-theory { }; + ceres = callPackage ../development/rocq-modules/ceres { }; + ceres-bs = callPackage ../development/rocq-modules/ceres-bs { }; + CertiRocq = callPackage ../development/rocq-modules/CertiRocq { }; + Cheerios = callPackage ../development/rocq-modules/Cheerios { }; + coinduction = callPackage ../development/rocq-modules/coinduction { }; + CoLoR = callPackage ../development/rocq-modules/CoLoR ( lib.optionalAttrs (lib.versions.isEq self.coq.coq-version "8.13") { bignums = self.bignums.override { version = "8.13.0"; }; } ); - compcert = callPackage ../development/coq-modules/compcert { + compcert = callPackage ../development/rocq-modules/compcert { inherit fetchpatch makeWrapper @@ -96,64 +96,64 @@ let stdenv ; }; - ConCert = callPackage ../development/coq-modules/ConCert { }; - coq-bits = callPackage ../development/coq-modules/coq-bits { }; - coq-elpi = callPackage ../development/coq-modules/coq-elpi { }; - rocq-elpi = callPackage ../development/coq-modules/coq-elpi { }; - coq-hammer = callPackage ../development/coq-modules/coq-hammer { }; - coq-hammer-tactics = callPackage ../development/coq-modules/coq-hammer/tactics.nix { }; - CoqMatrix = callPackage ../development/coq-modules/coq-matrix { }; - coq-haskell = callPackage ../development/coq-modules/coq-haskell { }; - coq-lsp = callPackage ../development/coq-modules/coq-lsp { }; - coq-record-update = callPackage ../development/coq-modules/coq-record-update { }; - coq-tactical = callPackage ../development/coq-modules/coq-tactical { }; - coqeal = callPackage ../development/coq-modules/coqeal ( + ConCert = callPackage ../development/rocq-modules/ConCert { }; + coq-bits = callPackage ../development/rocq-modules/coq-bits { }; + coq-elpi = callPackage ../development/rocq-modules/coq-elpi { }; + rocq-elpi = callPackage ../development/rocq-modules/coq-elpi { }; + coq-hammer = callPackage ../development/rocq-modules/coq-hammer { }; + coq-hammer-tactics = callPackage ../development/rocq-modules/coq-hammer/tactics.nix { }; + CoqMatrix = callPackage ../development/rocq-modules/coq-matrix { }; + coq-haskell = callPackage ../development/rocq-modules/coq-haskell { }; + coq-lsp = callPackage ../development/rocq-modules/coq-lsp { }; + coq-record-update = callPackage ../development/rocq-modules/coq-record-update { }; + coq-tactical = callPackage ../development/rocq-modules/coq-tactical { }; + coqeal = callPackage ../development/rocq-modules/coqeal ( lib.optionalAttrs (lib.versions.range "8.13" "8.14" self.coq.coq-version) { bignums = self.bignums.override { version = "${self.coq.coq-version}.0"; }; } ); - coqhammer = callPackage ../development/coq-modules/coqhammer { }; - coqide = callPackage ../development/coq-modules/coqide { }; - coqprime = callPackage ../development/coq-modules/coqprime { }; - coqtail-math = callPackage ../development/coq-modules/coqtail-math { }; - coquelicot = callPackage ../development/coq-modules/coquelicot { }; - coqutil = callPackage ../development/coq-modules/coqutil { }; - coqfmt = callPackage ../development/coq-modules/coqfmt { }; - corn = callPackage ../development/coq-modules/corn { }; - deriving = callPackage ../development/coq-modules/deriving { }; - dpdgraph = callPackage ../development/coq-modules/dpdgraph { }; - ElmExtraction = callPackage ../development/coq-modules/ElmExtraction { }; - equations = callPackage ../development/coq-modules/equations { }; - ExtLib = callPackage ../development/coq-modules/ExtLib { }; - extructures = callPackage ../development/coq-modules/extructures { }; - fcsl-pcm = callPackage ../development/coq-modules/fcsl-pcm { }; - flocq = callPackage ../development/coq-modules/flocq { }; - fourcolor = callPackage ../development/coq-modules/fourcolor { }; - gaia = callPackage ../development/coq-modules/gaia { }; - gaia-hydras = callPackage ../development/coq-modules/gaia-hydras { }; - gappalib = callPackage ../development/coq-modules/gappalib { }; - goedel = callPackage ../development/coq-modules/goedel { }; - graph-theory = callPackage ../development/coq-modules/graph-theory { }; - heq = callPackage ../development/coq-modules/heq { }; + coqhammer = callPackage ../development/rocq-modules/coqhammer { }; + coqide = callPackage ../development/rocq-modules/coqide { }; + coqprime = callPackage ../development/rocq-modules/coqprime { }; + coqtail-math = callPackage ../development/rocq-modules/coqtail-math { }; + coquelicot = callPackage ../development/rocq-modules/coquelicot { }; + coqutil = callPackage ../development/rocq-modules/coqutil { }; + coqfmt = callPackage ../development/rocq-modules/coqfmt { }; + corn = callPackage ../development/rocq-modules/corn { }; + deriving = callPackage ../development/rocq-modules/deriving { }; + dpdgraph = callPackage ../development/rocq-modules/dpdgraph { }; + ElmExtraction = callPackage ../development/rocq-modules/ElmExtraction { }; + equations = callPackage ../development/rocq-modules/equations { }; + ExtLib = callPackage ../development/rocq-modules/ExtLib { }; + extructures = callPackage ../development/rocq-modules/extructures { }; + fcsl-pcm = callPackage ../development/rocq-modules/fcsl-pcm { }; + flocq = callPackage ../development/rocq-modules/flocq { }; + fourcolor = callPackage ../development/rocq-modules/fourcolor { }; + gaia = callPackage ../development/rocq-modules/gaia { }; + gaia-hydras = callPackage ../development/rocq-modules/gaia-hydras { }; + gappalib = callPackage ../development/rocq-modules/gappalib { }; + goedel = callPackage ../development/rocq-modules/goedel { }; + graph-theory = callPackage ../development/rocq-modules/graph-theory { }; + heq = callPackage ../development/rocq-modules/heq { }; hierarchy-builder = callPackage ../development/rocq-modules/hierarchy-builder { }; - high-school-geometry = callPackage ../development/coq-modules/high-school-geometry { }; - HoTT = callPackage ../development/coq-modules/HoTT { }; - http = callPackage ../development/coq-modules/http { }; - hydra-battles = callPackage ../development/coq-modules/hydra-battles { }; - interval = callPackage ../development/coq-modules/interval { }; - InfSeqExt = callPackage ../development/coq-modules/InfSeqExt { }; + high-school-geometry = callPackage ../development/rocq-modules/high-school-geometry { }; + HoTT = callPackage ../development/rocq-modules/HoTT { }; + http = callPackage ../development/rocq-modules/http { }; + hydra-battles = callPackage ../development/rocq-modules/hydra-battles { }; + interval = callPackage ../development/rocq-modules/interval { }; + InfSeqExt = callPackage ../development/rocq-modules/InfSeqExt { }; iris = callPackage ../development/rocq-modules/iris { }; - iris-named-props = callPackage ../development/coq-modules/iris-named-props { }; - itauto = callPackage ../development/coq-modules/itauto { }; - ITree = callPackage ../development/coq-modules/ITree { }; - itree-io = callPackage ../development/coq-modules/itree-io { }; - jasmin = callPackage ../development/coq-modules/jasmin { }; - json = callPackage ../development/coq-modules/json { }; - lemma-overloading = callPackage ../development/coq-modules/lemma-overloading { }; - LibHyps = callPackage ../development/coq-modules/LibHyps { }; + iris-named-props = callPackage ../development/rocq-modules/iris-named-props { }; + itauto = callPackage ../development/rocq-modules/itauto { }; + ITree = callPackage ../development/rocq-modules/ITree { }; + itree-io = callPackage ../development/rocq-modules/itree-io { }; + jasmin = callPackage ../development/rocq-modules/jasmin { }; + json = callPackage ../development/rocq-modules/json { }; + lemma-overloading = callPackage ../development/rocq-modules/lemma-overloading { }; + LibHyps = callPackage ../development/rocq-modules/LibHyps { }; libvalidsdp = self.validsdp.libvalidsdp; - ltac2 = callPackage ../development/coq-modules/ltac2 { }; - math-classes = callPackage ../development/coq-modules/math-classes { }; + ltac2 = callPackage ../development/rocq-modules/ltac2 { }; + math-classes = callPackage ../development/rocq-modules/math-classes { }; mathcomp = callPackage ../development/rocq-modules/mathcomp { }; ssreflect = self.mathcomp.ssreflect; mathcomp-boot = self.mathcomp.boot; @@ -166,24 +166,24 @@ let mathcomp-field = self.mathcomp.field; mathcomp-group-representation = self.mathcomp.group-representation; mathcomp-character = self.mathcomp.group-representation; - mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel { }; - mathcomp-algebra-tactics = callPackage ../development/coq-modules/mathcomp-algebra-tactics { }; + mathcomp-abel = callPackage ../development/rocq-modules/mathcomp-abel { }; + mathcomp-algebra-tactics = callPackage ../development/rocq-modules/mathcomp-algebra-tactics { }; mathcomp-analysis = callPackage ../development/rocq-modules/mathcomp-analysis { }; mathcomp-analysis-stdlib = self.mathcomp-analysis.analysis-stdlib; - mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery { }; + mathcomp-apery = callPackage ../development/rocq-modules/mathcomp-apery { }; mathcomp-bigenough = callPackage ../development/rocq-modules/mathcomp-bigenough { }; mathcomp-classical = self.mathcomp-analysis.classical; mathcomp-experimental-reals = self.mathcomp-analysis.experimental-reals; mathcomp-finmap = callPackage ../development/rocq-modules/mathcomp-finmap { }; - mathcomp-infotheo = callPackage ../development/coq-modules/mathcomp-infotheo { }; + mathcomp-infotheo = callPackage ../development/rocq-modules/mathcomp-infotheo { }; mathcomp-real-closed = callPackage ../development/rocq-modules/mathcomp-real-closed { }; mathcomp-reals = self.mathcomp-analysis.reals; mathcomp-reals-stdlib = self.mathcomp-analysis.reals-stdlib; - mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan { }; - mathcomp-word = callPackage ../development/coq-modules/mathcomp-word { }; - mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify { }; - MenhirLib = callPackage ../development/coq-modules/MenhirLib { }; - metacoq = callPackage ../development/coq-modules/metacoq { }; + mathcomp-tarjan = callPackage ../development/rocq-modules/mathcomp-tarjan { }; + mathcomp-word = callPackage ../development/rocq-modules/mathcomp-word { }; + mathcomp-zify = callPackage ../development/rocq-modules/mathcomp-zify { }; + MenhirLib = callPackage ../development/rocq-modules/MenhirLib { }; + metacoq = callPackage ../development/rocq-modules/metacoq { }; metacoq-utils = self.metacoq.utils; metacoq-common = self.metacoq.common; metacoq-template-coq = self.metacoq.template-coq; @@ -195,8 +195,8 @@ let metacoq-safechecker-plugin = self.metacoq.safechecker-plugin; metacoq-erasure-plugin = self.metacoq.erasure-plugin; metacoq-translations = self.metacoq.translations; - metalib = callPackage ../development/coq-modules/metalib { }; - metarocq = callPackage ../development/coq-modules/metarocq { }; + metalib = callPackage ../development/rocq-modules/metalib { }; + metarocq = callPackage ../development/rocq-modules/metarocq { }; metarocq-utils = self.metarocq.utils; metarocq-common = self.metarocq.common; metarocq-template-rocq = self.metarocq.template-rocq; @@ -208,54 +208,54 @@ let metarocq-safechecker-plugin = self.metarocq.safechecker-plugin; metarocq-erasure-plugin = self.metarocq.erasure-plugin; metarocq-translations = self.metarocq.translations; - mtac2 = callPackage ../development/coq-modules/mtac2 { }; - multinomials = callPackage ../development/coq-modules/multinomials { }; - odd-order = callPackage ../development/coq-modules/odd-order { }; - Ordinal = callPackage ../development/coq-modules/Ordinal { }; - paco = callPackage ../development/coq-modules/paco { }; - paramcoq = callPackage ../development/coq-modules/paramcoq { }; - parsec = callPackage ../development/coq-modules/parsec { }; + mtac2 = callPackage ../development/rocq-modules/mtac2 { }; + multinomials = callPackage ../development/rocq-modules/multinomials { }; + odd-order = callPackage ../development/rocq-modules/odd-order { }; + Ordinal = callPackage ../development/rocq-modules/Ordinal { }; + paco = callPackage ../development/rocq-modules/paco { }; + paramcoq = callPackage ../development/rocq-modules/paramcoq { }; + parsec = callPackage ../development/rocq-modules/parsec { }; parseque = callPackage ../development/rocq-modules/parseque { }; - pocklington = callPackage ../development/coq-modules/pocklington { }; - QuickChick = callPackage ../development/coq-modules/QuickChick { }; - reglang = callPackage ../development/coq-modules/reglang { }; + pocklington = callPackage ../development/rocq-modules/pocklington { }; + QuickChick = callPackage ../development/rocq-modules/QuickChick { }; + reglang = callPackage ../development/rocq-modules/reglang { }; relation-algebra = callPackage ../development/rocq-modules/relation-algebra { }; - rewriter = callPackage ../development/coq-modules/rewriter { }; - RustExtraction = callPackage ../development/coq-modules/RustExtraction { }; - semantics = callPackage ../development/coq-modules/semantics { }; - serapi = callPackage ../development/coq-modules/serapi { }; - simple-io = callPackage ../development/coq-modules/simple-io { }; - smpl = callPackage ../development/coq-modules/smpl { }; - smtcoq = callPackage ../development/coq-modules/smtcoq { }; - ssprove = callPackage ../development/coq-modules/ssprove { }; - stalmarck-tactic = callPackage ../development/coq-modules/stalmarck { }; + rewriter = callPackage ../development/rocq-modules/rewriter { }; + RustExtraction = callPackage ../development/rocq-modules/RustExtraction { }; + semantics = callPackage ../development/rocq-modules/semantics { }; + serapi = callPackage ../development/rocq-modules/serapi { }; + simple-io = callPackage ../development/rocq-modules/simple-io { }; + smpl = callPackage ../development/rocq-modules/smpl { }; + smtcoq = callPackage ../development/rocq-modules/smtcoq { }; + ssprove = callPackage ../development/rocq-modules/ssprove { }; + stalmarck-tactic = callPackage ../development/rocq-modules/stalmarck { }; stalmarck = self.stalmarck-tactic.stalmarck; stdlib = callPackage ../development/rocq-modules/stdlib { }; stdpp = callPackage ../development/rocq-modules/stdpp { }; - StructTact = callPackage ../development/coq-modules/StructTact { }; - tlc = callPackage ../development/coq-modules/tlc { }; - topology = callPackage ../development/coq-modules/topology { }; - trakt = callPackage ../development/coq-modules/trakt { }; - TypedExtraction = callPackage ../development/coq-modules/TypedExtraction { }; + StructTact = callPackage ../development/rocq-modules/StructTact { }; + tlc = callPackage ../development/rocq-modules/tlc { }; + topology = callPackage ../development/rocq-modules/topology { }; + trakt = callPackage ../development/rocq-modules/trakt { }; + TypedExtraction = callPackage ../development/rocq-modules/TypedExtraction { }; TypedExtraction-common = self.TypedExtraction.common; TypedExtraction-elm = self.TypedExtraction.elm; TypedExtraction-rust = self.TypedExtraction.rust; TypedExtraction-plugin = self.TypedExtraction.plugin; - unicoq = callPackage ../development/coq-modules/unicoq { }; - validsdp = callPackage ../development/coq-modules/validsdp { }; - vcfloat = callPackage ../development/coq-modules/vcfloat ( + unicoq = callPackage ../development/rocq-modules/unicoq { }; + validsdp = callPackage ../development/rocq-modules/validsdp { }; + vcfloat = callPackage ../development/rocq-modules/vcfloat ( lib.optionalAttrs (lib.versions.range "8.16" "8.18" self.coq.version) { interval = self.interval.override { version = "4.9.0"; }; } ); - Velisarios = callPackage ../development/coq-modules/Velisarios { }; - Verdi = callPackage ../development/coq-modules/Verdi { }; - verified-extraction = callPackage ../development/coq-modules/verified-extraction { }; - Vpl = callPackage ../development/coq-modules/Vpl { }; - VplTactic = callPackage ../development/coq-modules/VplTactic { }; - vscoq-language-server = callPackage ../development/coq-modules/vscoq-language-server { }; + Velisarios = callPackage ../development/rocq-modules/Velisarios { }; + Verdi = callPackage ../development/rocq-modules/Verdi { }; + verified-extraction = callPackage ../development/rocq-modules/verified-extraction { }; + Vpl = callPackage ../development/rocq-modules/Vpl { }; + VplTactic = callPackage ../development/rocq-modules/VplTactic { }; + vscoq-language-server = callPackage ../development/rocq-modules/vscoq-language-server { }; vsrocq-language-server = callPackage ../development/rocq-modules/vsrocq-language-server { }; - VST = callPackage ../development/coq-modules/VST ( + VST = callPackage ../development/rocq-modules/VST ( (lib.optionalAttrs (lib.versionAtLeast self.coq.version "8.14") { compcert = self.compcert.override { version = @@ -279,9 +279,9 @@ let }; }) ); - wasmcert = callPackage ../development/coq-modules/wasmcert { }; - waterproof = callPackage ../development/coq-modules/waterproof { }; - zorns-lemma = callPackage ../development/coq-modules/zorns-lemma { }; + wasmcert = callPackage ../development/rocq-modules/wasmcert { }; + waterproof = callPackage ../development/rocq-modules/waterproof { }; + zorns-lemma = callPackage ../development/rocq-modules/zorns-lemma { }; filterPackages = doesFilter: if doesFilter then filterCoqPackages self else self; };