diff options
| author | Armaël Guéneau | 2018-05-31 14:17:39 +0200 |
|---|---|---|
| committer | Armaël Guéneau | 2018-05-31 14:17:39 +0200 |
| commit | 852e6f960d3fc6d4cf702ab21cfe813d9edbb531 (patch) | |
| tree | ecbfed9a6840ad8e908bedcf34522968f6408eba /tactics/hints.mli | |
| parent | ac8a84e3b4dc530b000e17b72c7e26f7a957420f (diff) | |
Refactor parsing rules for Hint Resolve -> and Hint Resolve <-
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 7ef7f01858..e958f986e2 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -83,6 +83,7 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.reference list * int option | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.reference list | HintsTransparency of Libnames.reference list * bool |