From 1f2de88e09c7bb1c0aa111db0d7d50b83f8a62d4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Aug 2017 18:02:57 +0200
Subject: Exporting the rewrite tactic.

---
 src/tac2tactics.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/tac2tactics.ml')

diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 439250db78..e7e15544af 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -44,3 +44,16 @@ let map_induction_clause ((clear, arg), eqn, as_, occ) =
 let induction_destruct isrec ev ic using =
   let ic = List.map map_induction_clause ic in
   Tactics.induction_destruct isrec ev (ic, using)
+
+type rewriting =
+  bool option *
+  multi *
+  EConstr.constr with_bindings tactic
+
+let rewrite ev rw cl by =
+  let map_rw (orient, repeat, c) =
+    (Option.default true orient, repeat, None, delayed_of_tactic c)
+  in
+  let rw = List.map map_rw rw in
+  let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
+  Equality.general_multi_rewrite ev rw cl by
-- 
cgit v1.2.3