package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/extraction_plugin/Extraction_plugin/Extract_env/index.html

Module `Extraction_plugin.Extract_env`Source

Source

val simple_extraction : 
  opaque_access:Global.indirect_accessor ->
  Libnames.qualid ->
  unit

Source

val full_extraction : 
  opaque_access:Global.indirect_accessor ->
  string option ->
  Libnames.qualid list ->
  unit

Source

val separate_extraction : 
  opaque_access:Global.indirect_accessor ->
  Libnames.qualid list ->
  unit

Source

val extraction_library : 
  opaque_access:Global.indirect_accessor ->
  bool ->
  Names.lident ->
  unit

Source

val extract_and_compile : 
  opaque_access:Global.indirect_accessor ->
  Libnames.qualid list ->
  unit

Source

val mono_environment : 
  Common.State.t ->
  opaque_access:Global.indirect_accessor ->
  Miniml.global list ->
  Names.ModPath.t list ->
  Miniml.ml_structure

Source

val print_one_decl : 
  Common.State.t ->
  Miniml.ml_structure ->
  Names.ModPath.t ->
  Miniml.ml_decl ->
  Pp.t

Sourceval show_extraction : pstate:Declare.Proof.t -> unit

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/extraction_plugin/Extraction_plugin/Extract_env/index.html

Module Extraction_plugin.Extract_envSource

dune-project
Dependency

Module `Extraction_plugin.Extract_env`Source