From 9efd7ac0311f2b55756d7aa2790b0adb75c69579 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 20 Feb 2018 15:13:26 +0100 Subject: tactics: export e_reduct_in_concl --- tactics/tactics.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'tactics/tactics.mli') diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 100ddf17f..5a29ff694 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -130,7 +130,8 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic (** {6 Reduction tactics. } *) -type tactic_reduction = env -> evar_map -> constr -> constr +type tactic_reduction = Reductionops.reduction_function +type e_tactic_reduction = Reductionops.e_reduction_function type change_arg = patvar_map -> evar_map -> evar_map * constr @@ -138,6 +139,7 @@ val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic val reduct_in_concl : tactic_reduction * cast_kind -> unit Proofview.tactic +val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> -- cgit v1.2.3