From 852e6f960d3fc6d4cf702ab21cfe813d9edbb531 Mon Sep 17 00:00:00 2001 From: Armaël Guéneau Date: Thu, 31 May 2018 14:17:39 +0200 Subject: Refactor parsing rules for Hint Resolve -> and Hint Resolve <- --- tactics/hints.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'tactics/hints.mli') diff --git a/tactics/hints.mli b/tactics/hints.mli index 7ef7f0185..e958f986e 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 -- cgit v1.2.3