From de88ba86e9d2a77883365503759eaec96928e9c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Aug 2017 17:21:42 +0200
Subject: Introducing quotations for the rewrite tactic.

---
 src/tac2qexpr.mli | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 0eb9e9f4b5..f6b8c2c19b 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -63,8 +63,10 @@ type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_fl
 type clause =
   { q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
 
+type constr_with_bindings = (Constrexpr.constr_expr * bindings) located
+
 type destruction_arg =
-| QElimOnConstr of (Constrexpr.constr_expr * bindings) located
+| QElimOnConstr of constr_with_bindings
 | QElimOnIdent of Id.t located
 | QElimOnAnonHyp of int located
 
@@ -76,3 +78,19 @@ type induction_clause_r = {
 }
 
 type induction_clause = induction_clause_r located
+
+type multi_r =
+| QPrecisely of int located
+| QUpTo of int located
+| QRepeatStar
+| QRepeatPlus
+
+type multi = multi_r located
+
+type rewriting_r = {
+  rew_orient : bool option located;
+  rew_repeat : multi;
+  rew_equatn : constr_with_bindings;
+}
+
+type rewriting = rewriting_r located
-- 
cgit v1.2.3