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

shelf : Evar.t list;

A representation of the shelf

given_up : Evar.t list;

A representation of the given up goals

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 -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
val dependent_start : name:Names.Id.t -> poly:bool -> Proofview.telescope -> t
val is_done : t -> bool
val is_complete : t -> bool
val partial_proof : t -> EConstr.constr list
val compact : t -> t
type open_error_reason =
| UnfinishedProof
| HasGivenUpGoals
exception OpenProof of Names.Id.t option * open_error_reason
val return : ?⁠pid:Names.Id.t -> t -> Evd.evar_map
type 'a focus_kind
val new_focus_kind : unit -> '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 : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t
exception FullyUnfocused
exception CannotUnfocusThisWay
exception NoSuchGoals of int * int
val unfocus : 'a focus_kind -> t -> unit -> t
val unfocused : t -> bool
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 pr_proof : t -> Pp.t
module V82 : sig ... end
val all_goals : t -> Goal.Set.t