diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 8dd0e34740..ce31a4dcc7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -171,7 +171,8 @@ val old_induct : quantified_hypothesis -> tactic val general_elim_in : identifier -> constr * constr substitution -> constr * constr substitution -> tactic -val new_induct : constr induction_arg -> constr with_bindings option -> tactic +val new_induct : constr induction_arg -> constr with_bindings option -> + identifier list list -> tactic (*s Case analysis tactics. *) @@ -179,7 +180,8 @@ val general_case_analysis : constr with_bindings -> tactic val simplest_case : constr -> tactic val old_destruct : quantified_hypothesis -> tactic -val new_destruct : constr induction_arg -> constr with_bindings option ->tactic +val new_destruct : constr induction_arg -> constr with_bindings option -> + identifier list list -> tactic (*s Eliminations giving the type instead of the proof. *) |