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=5cd48e23a8893f71f7b599dc919ce52d19eb4a6feeaa49f954e0a7123496a306

sha512=cc09f481c5dfdf181711aa13ef1d93176b4143a14ef863375f98e25db15da8ed4335526a27ba33479594a0bd745733eaaf02437ce7e0f972d97673b04d25773c

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