type t = goal
val ctxt : goal -> Core.Term.ctxt

ctxt g returns the typing context of the goal g.

val env : goal -> Core.Env.t

env g returns the scoping environment of the goal g.

val of_meta : Core.Term.meta -> goal

of_meta m creates a goal from the meta m.

val simpl : ( Core.Term.term -> Core.Term.term ) -> goal -> goal

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

val bindlib_ctxt : goal -> Bindlib.ctxt

bindlib_ctxt g computes a Bindlib context from a goal.

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

val hyps : goal Lplib.Base.pp

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