From 62a552b508b747b6cdf4bd818233f001ae4ce555 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 15 Sep 2014 21:33:48 +0200 Subject: Add a "Hint Mode ref (+ | -)*" hint for setting a global mode of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases). --- test-suite/success/auto.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index fb9f8c218..db3b19af5 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -24,3 +24,24 @@ auto using (pair O). Undo. eauto using (pair O). Qed. + +Create HintDb test discriminated. + +Parameter foo : forall x, x = x + 0. +Hint Resolve foo : test. + +Variable C : nat -> Type -> Prop. + +Variable c_inst : C 0 nat. + +Hint Resolve c_inst : test. + +Hint Mode C - + : test. +Hint Resolve c_inst : test2. +Hint Mode C + + : test2. + +Goal exists n, C n nat. +Proof. + eexists. Fail progress debug eauto with test2. + progress eauto with test. +Qed. -- cgit v1.2.3