package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type recipe = {

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

}

type inline = bool

type result = {

cook_body : Declarations.constant_def;
cook_type : Constr.types;
cook_proj : Declarations.projection_body option;
cook_universes : Declarations.constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;

}

val cook_constant : hcons:bool -> Environ.env -> recipe -> result

val cook_constr : Opaqueproof.cooking_info -> Constr.constr -> Constr.constr

val expmod_constr : Opaqueproof.work_list -> Constr.constr -> Constr.constr