diff options
| author | Enrico Tassi | 2020-09-25 18:09:25 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-10-09 17:09:02 +0200 |
| commit | a023009ba68c70d8654b29bd2f68631cc5536ba9 (patch) | |
| tree | 983ea49752ce4fdee40de82c95bc51377420d660 /plugins/ltac/tacinterp.mli | |
| parent | 39fe24769d18c21379f1123754fd606cdf8cd4c8 (diff) | |
[stm] move par: implementation to vernac/comTactic and stm/partac
The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).
This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index cbb17bf0fa..01d7306c9d 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) +type tactic_expr = { + global: bool; + ast: Tacexpr.raw_tactic_expr; +} -val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic +val hide_interp : tactic_expr ComTactic.tactic_interpreter (** Internals that can be useful for syntax extensions. *) |