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 =
  Declarations.constant_def
  * Declarations.constant_type
  * Declarations.projection_body option
  * Declarations.constant_universes
  * inline
  * Context.Named.t option

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

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

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