Subproofval refine_by_tactic : name:Names.Id.t -> poly:PolyFlags.t -> Environ.env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> EConstr.constr * Evd.evar_mapA variant of Proof.solve 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.
val build_by_tactic : Environ.env -> uctx:UState.t -> poly:PolyFlags.t -> typ:EConstr.types -> unit Proofview.tactic -> Constr.constr * Constr.types * UState.named_universes_entry * bool * UState.tSemantics of this function is a bit dubious, use with care
val build_by_tactic_opt : Environ.env -> uctx:UState.t -> poly:PolyFlags.t -> typ:EConstr.types ->
unit Proofview.tactic -> (Constr.constr * Constr.types * UState.named_universes_entry * bool * UState.t) optionSame as above but returns None rather than an exception if the proof is not finished
val declare_abstract : name:Names.Id.t -> poly:PolyFlags.t -> sign:EConstr.named_context -> secsign:Environ.named_context_val -> opaque:bool ->
solve_tac:unit Proofview.tactic -> Environ.env -> Evd.evar_map -> EConstr.t -> Evd.evar_map * EConstr.t * EConstr.t list * boolval shrink_entry : ('a, 'b, 'c) Context.Named.Declaration.pt list -> Constr.constr -> Constr.types -> Constr.constr * Constr.constr * EConstr.t list