diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 851c33e7a..faa8c4150 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -39,6 +39,9 @@ val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> open_constr with_bindings list -> tactic +val h_apply_in : advanced_flag -> evars_flag -> + open_constr with_bindings list -> + identifier * intro_pattern_expr located option -> tactic val h_elim : evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic |