Module Proof.GoalSource

ctxt g returns the typing context of the goal g.

env g returns the scoping environment of the goal g.

of_meta m creates a goal from the meta m.

simpl f g simplifies the goal g with the function f.

bindlib_ctxt g computes a Bindlib context from a goal.

pp ppf g prints on ppf the goal g without its hypotheses.

hyps ppf g prints on ppf the hypotheses of the goal g.