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/typeclasses/backtrack.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'test-suite/typeclasses') diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v index 112112f0c..fff740edd 100644 --- a/test-suite/typeclasses/backtrack.v +++ b/test-suite/typeclasses/backtrack.v @@ -1,5 +1,3 @@ -Set Typeclasses Strict Resolution. - (* Set Typeclasses Unique Instances *) (** This lets typeclass search assume that instance heads are unique, so if one matches no other need to be tried, @@ -14,6 +12,10 @@ Set Typeclasses Unique Instances. (* Unique *) Class D. Class C (A : Type) := c : A. + +Hint Mode C +. +Fail Definition test := c. + Unset Typeclasses Unique Instances. Instance : B -> D -> C nat := fun _ _ => 0. Instance : A -> D -> C nat := fun _ _ => 0. -- cgit v1.2.3