diff options
| author | Hugo Herbelin | 2020-05-09 15:09:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-09 15:09:54 +0200 |
| commit | 5681ea2535bbaef18e55d9bdc4270e12856de114 (patch) | |
| tree | 752c4cf3540125bacb57f903e32c1b17ea2214f9 /plugins/ltac/tacinterp.mli | |
| parent | 86afb971718d856007f503c9f059532ccbd3f5a5 (diff) | |
| parent | c39b622a8d8b32f335ee7dfe56ad27f9db7caaee (diff) | |
Merge PR #12204: Ltac helper functions API
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 *) |