diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-28 10:27:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-28 11:02:39 +0200 |
| commit | eb72574e1b526827706ee06206eb4a9626af3236 (patch) | |
| tree | bd57a11aa779c396b2eceb28a5764cf3bc5243af /theories/Classes | |
| parent | 16a6be0332bf3bea4a87ee5eec874cbf444174c3 (diff) | |
Typeclasses: use once in by clause for typeclass eauto
Otherwise we may backtrack on the resolution in a
by which seems strange.
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Morphisms.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 607e7d10c..06511ace5 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -470,7 +470,7 @@ Ltac partial_application_tactic := end in let rec do_partial H ar m := - match ar with + lazymatch ar with | 0%nat => do_partial_apps H m ltac:(fail 1) | S ?n' => match m with @@ -483,7 +483,7 @@ Ltac partial_application_tactic := let n := fresh in evar (n:nat) ; let v := eval compute in n in clear n ; let H := fresh in - assert(H:Params m' v) by (subst m'; typeclasses eauto) ; + assert(H:Params m' v) by (subst m'; once typeclasses eauto) ; let v' := eval compute in v in subst m'; (sk H v' || fail 1)) || fk |