From 98703c8247fd86deab2d82a70c22d43797e4a548 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 10 Jun 2016 01:15:38 +0200 Subject: Extend Hint Mode to handle the no-head-evar case Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply. --- intf/vernacexpr.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'intf/vernacexpr.mli') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index faa5ba251..45d71e32b 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -118,12 +118,17 @@ type reference_or_constr = | HintsReference of reference | HintsConstr of constr_expr +type hint_mode = + | ModeInput (* No evars *) + | ModeNoHeadEvar (* No evar at the head *) + | ModeOutput (* Anything *) + type hints_expr = | HintsResolve of (int option * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool - | HintsMode of reference * bool list + | HintsMode of reference * hint_mode list | HintsConstructors of reference list | HintsExtern of int * constr_expr option * raw_tactic_expr -- cgit v1.2.3