From da28b6e65d9b9a74c277cb15055131c8a151bb72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 00:42:22 +0200
Subject: Quotations for auto-related tactics.

---
 src/tac2qexpr.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 577fe8edfe..4bbaf43d8d 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -125,3 +125,9 @@ type constr_match_branch_r =
 type constr_match_branch = constr_match_branch_r located
 
 type constr_matching = constr_match_branch list located
+
+type hintdb_r =
+| QHintAll
+| QHintDbs of Id.t located or_anti list
+
+type hintdb = hintdb_r located
-- 
cgit v1.2.3