Info.GoalsSourceWe move towards a more modular design here, for preprocessing
val get_goals_unit :
st:Coq.State.t ->
(unit Coq.Goals.Reified_goal.t, Pp.t) Coq.Goals.t optionval get_goals :
st:Coq.State.t ->
((Environ.env * Evd.evar_map * EConstr.t) Coq.Goals.Reified_goal.t, Pp.t)
Coq.Goals.t
optionval goals :
token:Coq.Limits.Token.t ->
st:Coq.State.t ->
(Pp.t Coq.Goals.reified_pp option, Loc.t) Coq.Protect.E.t