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 f4da57144..86a337678 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -78,8 +78,8 @@ val h_new_destruct : evars_flag -> Tacticals.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> (constr with_ebindings induction_arg list * constr with_ebindings option * - (intro_pattern_expr located option * intro_pattern_expr located option) * - Tacticals.clause option) list -> tactic + (intro_pattern_expr located option * intro_pattern_expr located option)) list + * Tacticals.clause option -> tactic val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic |