From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 24 Oct 2016 18:18:33 +0200
Subject: Lets Hints/Instances take an optional pattern

In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
---
 intf/vernacexpr.mli | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 1336c92b6f..92e4dd618e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -123,8 +123,14 @@ type hint_mode =
   | ModeNoHeadEvar (* No evar at the head *)
   | ModeOutput (* Anything *)
 
+type 'a hint_info_gen =
+    { hint_priority : int option;
+      hint_pattern : 'a option }
+
+type hint_info_expr = constr_pattern_expr hint_info_gen
+
 type hints_expr =
-  | HintsResolve of (int option * bool * reference_or_constr) list
+  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
@@ -368,12 +374,12 @@ type vernac_expr =
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(bool * constr_expr) option * (* props *)
-	int option (* Priority *)
+	hint_info_expr
 
   | VernacContext of local_binder list
 
   | VernacDeclareInstances of
-    reference list * int option (* instance names, priority *)
+    (reference * hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)
 
-- 
cgit v1.2.3