package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

Serialization library and protocol for machine interaction with the Coq proof assistant

Install

sha256=e252d05b41e920c1df4343c437be4018804971ecfd00291ddb4d31ce72281853

sha512=1f936181265346d0cd17ec292b98f201382ea84440b415b77664430044ba599072e653366f080d8b63ee5f8fe5bfc0d2cd2a38cc759532500d8c60a483fe36b7

Sourcetype 'a hyp = Names.Id.t list * 'a option * 'a

Sourcetype info = {

}

Sourcetype 'a reified_goal = {

}

Sourcetype 'a ser_goals = {

}

val get_goals_gen : 
  (Environ.env -> Evd.evar_map -> Constr.t -> 'a) ->
  doc:Stm.doc ->
  Stateid.t ->
  'a reified_goal ser_goals option

val get_goals : 
  doc:Stm.doc ->
  Stateid.t ->
  Constr.t reified_goal ser_goals option

val get_egoals : 
  doc:Stm.doc ->
  Stateid.t ->
  Constrexpr.constr_expr reified_goal ser_goals option