diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-10 18:58:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 15:13:25 -0400 |
| commit | 11aaa1fd8230a347f1dca1a0f349ea7c7f2768c3 (patch) | |
| tree | ab8285bfecf4a9d6b73b6a26ce4d1f182d5dbe55 /tactics/tactics.mli | |
| parent | adc2035410a339cfa88dae527b631f5131adaa54 (diff) | |
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.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 4 |
1 files changed, 3 insertions, 1 deletions
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 |