diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 3028d3a1e2..12791dfb5f 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -57,10 +57,11 @@ val h_cut : constr -> tactic val h_generalize : constr list -> tactic val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic val h_generalize_dep : constr -> tactic -val h_let_tac : letin_flag -> name -> constr -> - Locus.clause -> tactic +val h_let_tac : letin_flag -> name -> constr -> Locus.clause -> + intro_pattern_expr located option -> tactic val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> - Locus.clause -> tactic + Locus.clause -> intro_pattern_expr located option -> + tactic (** Derived basic tactics *) |