diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 47fd9aac2..b4491770e 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -54,11 +54,11 @@ val h_cofix : Id.t option -> tactic 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_gen : (constr Locus.with_occurrences * Name.t) list -> tactic val h_generalize_dep : ?with_let:bool -> constr -> tactic -val h_let_tac : letin_flag -> name -> constr -> Locus.clause -> +val h_let_tac : letin_flag -> Name.t -> constr -> Locus.clause -> intro_pattern_expr located option -> tactic -val h_let_pat_tac : letin_flag -> name -> evar_map * constr -> +val h_let_pat_tac : letin_flag -> Name.t -> evar_map * constr -> Locus.clause -> intro_pattern_expr located option -> tactic |