diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index cffe84252..3028d3a1e 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -68,19 +68,19 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic val h_new_induction : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> + (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> Locus.clause option -> tactic val h_new_destruct : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> + (evar_map * constr with_bindings) induction_arg -> intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> Locus.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg list * - constr with_bindings option * + ((evar_map * constr with_bindings) induction_arg * (intro_pattern_expr located option * intro_pattern_expr located option)) list + * constr with_bindings option * Locus.clause option -> tactic val h_specialize : int option -> constr with_bindings -> tactic |