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; };