Module `Pfedit`

val get_current_context : Declare.Proof.t -> Evd.evar_map * Environ.env
val solve : ?⁠with_end_tac:unit Proofview.tactic -> Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool
val by : unit Proofview.tactic -> Declare.Proof.t -> Declare.Proof.t * bool
val refine_by_tactic : name:Names.Id.t -> poly:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> Constr.constr * Evd.evar_map
val build_by_tactic : ?⁠side_eff:bool -> Environ.env -> uctx:UState.t -> poly:bool -> typ:EConstr.types -> unit Proofview.tactic -> Constr.constr * Constr.types option * bool * UState.t
val build_constant_by_tactic : name:Names.Id.t -> ?⁠opaque:Declare.opacity_flag -> uctx:UState.t -> sign:Environ.named_context_val -> poly:bool -> EConstr.types -> unit Proofview.tactic -> Evd.side_effects Declare.proof_entry * bool * UState.t