Module Proof

type t
type data = {
sigma : Evd.evar_map;(*

A representation of the evar_map EJGA wouldn't it better to just return the proofview?

*)
goals : Evar.t list;(*

Focused goals

*)
entry : Proofview.entry;(*

Entry for the proofview

*)
stack : (Evar.t list * Evar.t list) list;(*

A representation of the focus stack

*)
name : Names.Id.t;(*

The name of the theorem whose proof is being constructed

*)
poly : bool;(*

polymorphism

*)
}
val data : t -> data
val start : name:Names.Id.t -> poly:bool -> ?typing_flags:Declarations.typing_flags -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
val dependent_start : name:Names.Id.t -> poly:bool -> ?typing_flags:Declarations.typing_flags -> Proofview.telescope -> t
val is_done : t -> bool
val partial_proof : t -> EConstr.constr list
val compact : t -> t
val update_sigma_univs : UGraph.t -> t -> t

update_sigma_univs lifts UState.update_sigma_univs to the proof

type 'a focus_kind
val new_focus_kind : string -> 'a focus_kind
type 'a focus_condition
val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
val focus : 'a focus_condition -> 'a -> int -> t -> t
val focus_id : 'a focus_condition -> 'a -> Names.Id.t -> t -> t
exception FullyUnfocused
exception CannotUnfocusThisWay
exception NoSuchGoals of int * int
exception NoSuchGoal of Names.Id.t option
val unfocus : 'a focus_kind -> t -> unit -> t
val unfocused : t -> bool
val unfocus_all : t -> t

Unfocus everything (fail if no allowed).

exception NoSuchFocus
val get_at_focus : 'a focus_kind -> t -> 'a
val is_last_focus : 'a focus_kind -> t -> bool
val no_focused_goal : t -> bool
val run_tactic : Environ.env -> 'a Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree) * 'a
val maximal_unfocus : 'a focus_kind -> t -> t
val unshelve : t -> t
val goal_uid : Evar.t -> string
val pr_proof : t -> Pp.t
val background_subgoals : t -> Evar.t list
val all_goals : t -> Evar.Set.t

solve (SelectNth n) tac applies tactic tac to the nth subgoal of the current focused proof. solve SelectAll tac applies tac to all subgoals.

val solve : ?with_end_tac:unit Proofview.tactic -> Goal_select.t -> int option -> unit Proofview.tactic -> t -> t * bool
val use_unification_heuristics : unit -> bool

Option telling if unification heuristics should be used.

val refine_by_tactic : name:Names.Id.t -> poly:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> EConstr.constr * Evd.evar_map

A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad.

exception SuggestNoSuchGoals of int * t
val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env

Helpers to obtain proof state when in an interactive proof

val get_proof_context : t -> Evd.evar_map * Environ.env

get_proof_context () gets the goal context for the first subgoal of the proof