diff options
| author | Hugo Herbelin | 2020-10-29 14:11:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-29 15:07:52 +0100 |
| commit | c233a13620202790fa59fc720b7149a0d88f275a (patch) | |
| tree | 15818db55abb73e375fe869d77d62c2f5ba9eab3 /plugins/ltac/tacinterp.mli | |
| parent | 473160ebe4a835dde50d6c209ab17c7e1b84979c (diff) | |
Fixing interpretation of rewrite_strat argument in Ltac.
Ltac variables were not yet supported.
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index fe3079198c..a74f4592f7 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -77,6 +77,9 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic (** Interprets redexp arguments *) +val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> glob_red_expr -> Evd.evar_map * red_expr + +(** Interprets redexp arguments from a raw one *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr (** Interprets tactic expressions *) |