diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-15 21:33:48 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-15 21:37:31 +0200 |
commit | 62a552b508b747b6cdf4bd818233f001ae4ce555 (patch) | |
tree | 80feb19c8d02935b550c7f6c971ea42fc39020b2 /test-suite | |
parent | 1c113305039857ca219f252f5e80f4b179a39082 (diff) |
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).
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/auto.v | 21 | ||||
-rw-r--r-- | test-suite/typeclasses/backtrack.v | 6 |
2 files changed, 25 insertions, 2 deletions
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. 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. |