diff options
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 *) |