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 declare_abstract : (name:Names.Id.t -> poly:bool -> kind:Decls.logical_kind -> sign:EConstr.named_context -> secsign:Environ.named_context_val -> opaque:bool -> solve_tac:unit Proofview.tactic -> Evd.evar_map -> EConstr.t -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool) Stdlib.ref