diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 11:33:40 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 11:33:40 +0200 |
| commit | d8cd9ba6d56d32eb8aa383bca9198a18517e82d3 (patch) | |
| tree | dc6670607c7831c5a6b80da427b1f299ffd0f2df /plugins/ltac/tacinterp.mli | |
| parent | 2de309b65b379a3c496752aa25f1cfc177644222 (diff) | |
| parent | e2e23a52655fbd04a1cc659e64fb520d97d7f9db (diff) | |
Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index fd2d96bd6..f9883e444 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -28,6 +28,7 @@ sig val to_list : t -> t list option val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a + val apply : t -> t list -> unit Proofview.tactic end (** Values for interpretation *) |