From 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Jun 2016 18:58:24 -0400 Subject: Add support for transparent abstract (no syntax) This is a small change that allows a transparent version of tclABSTRACT. Additionally, it factors the machinery of [abstract] through a plugin-accessible function which allows alternate continuations (other than exact_no_check. It might be nice to factor it further, into a cache_term function that caches a term, and a separate bit that calls cache_term with the result of running the tactic. --- tactics/tactics.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'tactics/tactics.mli') diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ba4a9706d..d206011ee 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -401,7 +401,9 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic +val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic + +val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic -- cgit v1.2.3