You are viewing the staging branch of the website @ b4332b8, not the live version.

package rocq-typed-extraction-common

Overview
Doc

You can search for identifiers within the package.

in-package search v0.2.0

Rocq extraction to Rust and Elm

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

T

The COBRA team

Maintainers

D

Danil Annenkov <danil.v.annenkov@gmail.com>

Sources

sha512=4dd884edc9d4f6ad3a23305c5359a39d6208186c020503e0eb1db98a723eb89bfc0d5bc2d38013d2e8dec95efe6200e803c3999a8dd6046547237761010dded4

Description

A framework for extracting Rocq programs to Rust and Elm

Tags

keyword:extraction logpath:TypedExtraction

Published: 13 Mar 2026

Dependencies (9)

rocq-metarocq-erasure >= "1.5.1"
rocq-metarocq-safechecker >= "1.5.1"
rocq-metarocq-pcuic >= "1.5.1"
rocq-metarocq-template-pcuic >= "1.5.1"
rocq-metarocq-template >= "1.5.1"
rocq-metarocq-common >= "1.5.1"
rocq-metarocq-utils >= "1.5.1"
rocq-stdlib >= "9.0" & < "9.2~"
rocq-core >= "9.1" & < "9.2~"

Dev Dependencies

None

Used by (2)

rocq-elm-extraction >= "0.2.1"
rocq-rust-extraction >= "0.2.1"

Conflicts

None

On This Page

Description
Dependencies (9)
Dev Dependencies
Used by (2)
Conflicts