package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Main functions for translating module entries

type 'a vm_handler = {
  1. vm_handler : Environ.env -> Declarations.universes -> Constr.t -> 'a -> 'a * Vmlibrary.indirect_code option;
}
type 'a vm_state = 'a * 'a vm_handler

translate_module produces a module_body out of a module_entry. In the output fields:

  • mod_expr is Abstract for a MType entry, or Algebraic for MExpr.
  • mod_type_alg is None only for a MExpr without explicit signature.

translate_modtype produces a module_type_body whose mod_type_alg cannot be None (and of course mod_expr is Abstract).

From an already-translated (or interactive) implementation and an (optional) signature entry, produces a final module_body

translate_mse_incl translate the mse of a module or module type given to an Include

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct