SubproofSourceval 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