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/tac2entries.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/tac2entries.mli')

diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index f5c5a479c4..1fe13cda17 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -63,4 +63,5 @@ val q_intropattern : raw_tacexpr Pcoq.Gram.entry
 val q_intropatterns : raw_tacexpr Pcoq.Gram.entry
 val q_induction_clause : raw_tacexpr Pcoq.Gram.entry
 val q_rewriting : raw_tacexpr Pcoq.Gram.entry
+val q_clause : raw_tacexpr Pcoq.Gram.entry
 end
-- 
cgit v1.2.3