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=cf071a26d3857f82e3a8ece60afbfc18c2fee22f3ae16a5f84117f22f096ca13f867d0d2672f43f0b9e950741487722ef7a3fbff9c4d31a5dd34f35aea3b8c36

Description

A framework for extracting Rocq programs to Rust and Elm

Tags

keyword:extraction logpath:TypedExtraction

Published: 26 Feb 2026

Dependencies (9)

rocq-metarocq-erasure >= "1.4" & < "1.5"
rocq-metarocq-safechecker >= "1.4" & < "1.5"
rocq-metarocq-pcuic >= "1.4" & < "1.5"
rocq-metarocq-template-pcuic >= "1.4" & < "1.5"
rocq-metarocq-template >= "1.4" & < "1.5"
rocq-metarocq-common >= "1.4" & < "1.5"
rocq-metarocq-utils >= "1.4" & < "1.5"
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