diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 7a83eff5e..6b4a1cbc1 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -55,8 +55,10 @@ val h_instantiate : int -> constr -> tactic val h_old_induction : quantified_hypothesis -> tactic val h_old_destruct : quantified_hypothesis -> tactic -val h_new_induction : constr induction_arg -> tactic -val h_new_destruct : constr induction_arg -> tactic +val h_new_induction : + constr induction_arg -> constr with_bindings option -> tactic +val h_new_destruct : + constr induction_arg -> constr with_bindings option -> tactic val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic |