mk_goalstate : goal -> goalstate
Converts a goal into a 1-element goalstate.
Given a goal g, the call mk_goalstate g converts it into a goalstate with
that goal as its only member. (A goalstate consists of a list of subgoals as
well as justification and metavariable information.)
- FAILURE CONDITIONS
- SEE ALSO
g, set_goal, TAC_PROOF.