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.ml  | 3 ++-
 tactics/tactics.mli | 4 +++-
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 94622114dd..4b0b11e423 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -644,7 +644,8 @@ let cofix ido = match ido with
 (*          Reduction and conversion tactics                  *)
 (**************************************************************)
 
-type tactic_reduction = env -> evar_map -> constr -> constr
+type tactic_reduction = Reductionops.reduction_function
+type e_tactic_reduction = Reductionops.e_reduction_function
 
 let pf_reduce_decl redfun where decl gl =
   let open Context.Named.Declaration in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 100ddf17f2..5a29ff6946 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