aboutsummaryrefslogtreecommitdiff
path: root/src/tac2qexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2qexpr.mli')
-rw-r--r--src/tac2qexpr.mli6
1 files changed, 6 insertions, 0 deletions
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