diff options
| author | Pierre-Marie Pédrot | 2017-09-05 00:42:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 01:06:23 +0200 |
| commit | da28b6e65d9b9a74c277cb15055131c8a151bb72 (patch) | |
| tree | 38697f7a7ddebd9006bae72405131fe906c83a85 /src/tac2qexpr.mli | |
| parent | ebe95a28cf012aff33eb5ce167be6520e6643cfd (diff) | |
Quotations for auto-related tactics.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 6 |
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 |