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. ty : 'a;
  3. hyps : 'a hyp list;
}
Sourceval map_reified_goal : f:('a -> 'b) -> 'a reified_goal -> 'b reified_goal
Sourcetype '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;
}
Sourceval map_goals : f:('a -> 'b) -> 'a goals -> 'b goals
Sourcetype reified_pp = Pp.t reified_goal goals
Sourceval reify : ppx:(Environ.env -> Evd.evar_map -> EConstr.t -> 'a) -> State.Proof.t -> 'a reified_goal goals

Stm-independent goal processor