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.mli | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'src/tac2tactics.mli')

diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index f29793411a..93cc6ecd68 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Names
+open Locus
 open Misctypes
 open Tactypes
 open Proofview
@@ -21,7 +22,15 @@ type induction_clause =
   EConstr.constr with_bindings tactic destruction_arg *
   intro_pattern_naming option *
   or_and_intro_pattern option *
-  Locus.clause option
+  clause option
 
 val induction_destruct : rec_flag -> evars_flag ->
-  induction_clause list -> EConstr.constr with_bindings option -> unit Proofview.tactic
+  induction_clause list -> EConstr.constr with_bindings option -> unit tactic
+
+type rewriting =
+  bool option *
+  multi *
+  EConstr.constr with_bindings tactic
+
+val rewrite :
+  evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
-- 
cgit v1.2.3