diff options
| author | Pierre-Marie Pédrot | 2020-04-09 23:29:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-07 00:22:11 +0200 |
| commit | c39b622a8d8b32f335ee7dfe56ad27f9db7caaee (patch) | |
| tree | 6b8bd1218e3c31d1c85dd1d89a8243f61d6157de /plugins/ltac/tacinterp.mli | |
| parent | f694d42400593d7ef3ad6c2812395f941cc4f5ca (diff) | |
Export API to recover values out of Ltac application.
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 ce34356a37..cbb17bf0fa 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -29,6 +29,7 @@ sig 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 + val apply_val : t -> t list -> t Ftactic.t end (** Values for interpretation *) |