package coq-lsp

  1. Overview
  2. Docs
type 'a hyp = {
  1. names : Names.Id.t list;
  2. def : 'a option;
  3. ty : 'a;
}
type info = {
  1. evar : Evar.t;
  2. name : Names.Id.t option;
}
type 'a reified_goal = {
  1. info : info;
  2. ty : 'a;
  3. hyps : 'a hyp list;
}
type 'a goals = {
  1. goals : 'a list;
  2. stack : ('a list * 'a list) list;
  3. bullet : Pp.t option;
  4. shelf : 'a list;
  5. given_up : 'a list;
}
val process_goal_gen : (Environ.env -> Evd.evar_map -> Constr.t -> 'a) -> Evd.evar_map -> Evar.t -> 'a reified_goal

Stm-independent goal processor

type reified_pp = Pp.t reified_goal goals
val pp_goals : reified_pp -> Pp.t