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/g_ltac2.ml4 | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'src/g_ltac2.ml4')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 48a593df28..8b373647f3 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -309,7 +309,7 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 
 GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
-          q_rewriting;
+          q_rewriting q_clause;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -479,12 +479,14 @@ GEXTEND Gram
         { q_onhyps = Some hl; q_concl_occs = QNoOccurrences }
     ] ]
   ;
-  opt_clause:
-    [ [ "in"; cl = in_clause -> Some cl
-      | "at"; occs = occs_nums -> Some { q_onhyps = Some []; q_concl_occs = occs }
-      | -> None
+  clause:
+    [ [ "in"; cl = in_clause -> cl
+      | "at"; occs = occs_nums -> { q_onhyps = Some []; q_concl_occs = occs }
     ] ]
   ;
+  q_clause:
+    [ [ cl = clause -> Tac2quote.of_clause cl ] ]
+  ;
   concl_occ:
     [ [ "*"; occs = occs -> occs
       | -> QNoOccurrences
@@ -492,7 +494,7 @@ GEXTEND Gram
   ;
   induction_clause:
     [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
-        cl = opt_clause ->
+        cl = OPT clause ->
         Loc.tag ~loc:!@loc @@ {
           indcl_arg = c;
           indcl_eqn = eq;
-- 
cgit v1.2.3