Module Handle.ProofSource

Proofs and tactics.

Sourcetype goal_typ = {
  1. goal_meta : Core.Term.meta;
    (*

    Goal metavariable.

    *)
  2. goal_hyps : Core.Env.t;
    (*

    Precomputed scoping environment.

    *)
  3. goal_type : Core.Term.term;
    (*

    Precomputed type.

    *)
}

Type of goals.

Sourcetype goal =
  1. | Typ of goal_typ
    (*

    Typing goal.

    *)
  2. | Unif of Core.Term.constr
    (*

    Unification goal.

    *)
Sourceval is_typ : goal -> bool
Sourceval is_unif : goal -> bool
Sourceval get_constr : goal -> Core.Term.constr
Sourcemodule Goal : sig ... end
Sourceval add_goals_of_problem : Core.Term.problem -> goal list -> goal list

add_goals_of_problem p gs extends the list of goals gs with the metavariables and constraints of p.

Sourcetype proof_state = {
  1. proof_name : Common.Pos.strloc;
    (*

    Name of the theorem.

    *)
  2. proof_term : Core.Term.meta option;
    (*

    Optional metavariable holding the goal associated to a symbol used as a theorem/definition and not just a simple declaration

    *)
  3. proof_goals : goal list;
    (*

    Open goals (focused goal is first).

    *)
}

Representation of the proof state of a theorem.

Sourceval finished : proof_state -> bool

finished ps tells whether there are unsolved goals in ps.

goals ppf gl prints the goal list gl to channel ppf.

Sourceval remove_solved_goals : proof_state -> proof_state

remove_solved_goals ps removes from the proof state ps the typing goals that are solved.

Sourceval meta_of_key : proof_state -> int -> Core.Term.meta option

meta_of_key ps i returns Some m where m is a meta of ps whose key is i, or else it returns None.

Sourceval focus_env : proof_state option -> Core.Env.t

focus_env ps returns the scoping environment of the focused goal or the empty environment if there is none.