diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index dba9908a9..82146c01a 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -53,8 +53,8 @@ val h_instantiate : int -> constr -> tactic (* Derived basic tactics *) -val h_old_induction : quantified_hypothesis -> tactic -val h_old_destruct : quantified_hypothesis -> tactic +val h_simple_induction : quantified_hypothesis -> tactic +val h_simple_destruct : quantified_hypothesis -> tactic val h_new_induction : constr induction_arg -> constr with_bindings option -> intro_pattern_expr list list -> tactic |