From 852e6f960d3fc6d4cf702ab21cfe813d9edbb531 Mon Sep 17 00:00:00 2001
From: Armaël Guéneau <armael.gueneau@ens-lyon.fr>
Date: Thu, 31 May 2018 14:17:39 +0200
Subject: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-

---
 vernac/vernacexpr.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/vernacexpr.ml')

diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 4ff9d105b..5cba073db 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -124,6 +124,7 @@ type hint_info_expr = Hints.hint_info_expr
 
 type hints_expr = Hints.hints_expr =
   | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
+  | HintsResolveIFF of bool * reference list * int option
   | HintsImmediate of Hints.reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
-- 
cgit v1.2.3