diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 9d8a7e57c..c2c6bd778 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -103,6 +103,8 @@ val interp_tac_gen : (identifier * value) list -> (* Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr +val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr + val eval_tactic : glob_tactic_expr -> tactic val interp : raw_tactic_expr -> tactic |