package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.11.0+0.11.1.tbz
sha256=f06bb0ab1041ac6f8d73faddda404827ce94b6b3310483e93d7fd18bd018e1ed
sha512=ecbed7b5b8451f65d40bf50fd1471b5038029c6f1ae8912c8cb51e61699cc4c158bc4f3533ec5f0898d1fc3d91683c0ff815fa44be7fdaedea59b71ca1d1b7d3
doc/coq-serapi.serapi_v8_11/Serapi/Serapi_assumptions/index.html
Module Serapi.Serapi_assumptions
type t = {predicative : Declarations.set_predicativity;type_in_type : bool;vars : (Names.Id.t * Constr.t) list;axioms : (Printer.axiom * Constr.t * ax_ctx) list;opaque : (Names.Constant.t * Constr.t) list;trans : (Names.Constant.t * Constr.t) list;
}val build : Environ.env -> Constr.t Printer.ContextObjectMap.t -> tval print : Environ.env -> Evd.evar_map -> t -> Pp.t