package rocq-verified-extraction
Verified extraction from Rocq to OCaml
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0.0-9.1.tar.gz
sha512=65440c1ac351f99c7a0181feaf54614f0699a8ee55035133ed10de22ce8a8df5b3f2a7a216f86b6262ea1aa9940d5322957fe181c94f7d41a69ca3caa746bf5f
Description
Tags
keyword:extraction category:Miscellaneous/Rocq Extensions logpath:VerifiedExtractionPublished: 13 Mar 2026
Dependencies (6)
-
malfunction
>= "0.7.1" -
rocq-metarocq-erasure-plugin
>= "1.5.1" -
rocq-ceres-bytestring
>= "1.0.0" -
rocq-stdlib
>= "9.0" -
rocq-core
>= "9.1" -
ocaml
>= "4.13"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page