Module Coq.GoalsSource

Sourcetype 'a hyp = {
  1. names : string list;
    (*

    This will become Names.Id.t list in 0.2.0

    *)
  2. def : 'a option;
  3. ty : 'a;
}
Sourcetype info = {
  1. evar : Evar.t;
  2. name : Names.Id.t option;
}
Sourcetype 'a reified_goal = {
  1. info : info;
  2. hyps : 'a hyp list;
  3. ty : 'a;
}
Sourceval map_reified_goal : f:('a -> 'b) -> 'a reified_goal -> 'b reified_goal
Sourcetype ('a, 'pp) goals = {
  1. goals : 'a list;
  2. stack : ('a list * 'a list) list;
  3. bullet : 'pp option;
  4. shelf : 'a list;
  5. given_up : 'a list;
}
Sourceval map_goals : f:('a -> 'b) -> g:('pp -> 'pp') -> ('a, 'pp) goals -> ('b, 'pp') goals
Sourcetype 'pp reified_pp = ('pp reified_goal, 'pp) goals
Sourceval reify : ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'pp) -> State.Proof.t -> ('pp reified_goal, Pp.t) goals

Stm-independent goal processor