Module Abstract

val cache_term_by_tactic_then : opaque:bool -> name_op:Names.Id.t option -> ?goal_type:EConstr.constr option -> unit Proofview.tactic -> (EConstr.constr -> EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
val get_inline_abstract_subproof : unit -> bool