diff options
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index dba9c938ec..fe3079198c 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -126,12 +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 = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr -> ComTactic.interpretable +val hide_interp : ltac_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) |