package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.1.tar.gz

sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/coq-core.kernel/Cooking/index.html

Module `Cooking`Source

Cooking the constants.

Sourcetype recipe = {

from : Declarations.constant_body;
info : Declarations.cooking_info;

}

Sourcetype inline = bool

Sourcetype 'opaque result = {

cook_body : (Constr.constr, 'opaque) Declarations.constant_def;
cook_type : Constr.types;
cook_universes : Declarations.universes;
cook_relevance : Sorts.relevance;
cook_inline : inline;
cook_context : Names.Id.Set.t option;
cook_flags : Declarations.typing_flags;

}

Source

val cook_constant : 
  recipe ->
  Declarations.cooking_info Opaqueproof.opaque result

Source

val cook_constr : 
  Declarations.cooking_info list ->
  (Constr.constr * unit Opaqueproof.delayed_universes) ->
  Constr.constr * unit Opaqueproof.delayed_universes

Source

val cook_inductive : 
  Declarations.cooking_info ->
  Declarations.mutual_inductive_body ->
  Declarations.mutual_inductive_body

Utility functions used in module `Discharge`.

Sourceval expmod_constr : Declarations.work_list -> Constr.constr -> Constr.constr

On This Page

Cooking the constants.
Utility functions used in module Discharge.

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Cooking/index.html

Module CookingSource

Cooking the constants.

Utility functions used in module Discharge.

Module `Cooking`Source

Utility functions used in module `Discharge`.