diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Morphisms.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 81b31d783..607e7d10c 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -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 typeclasses eauto ; + assert(H:Params m' v) by (subst m'; typeclasses eauto) ; let v' := eval compute in v in subst m'; (sk H v' || fail 1)) || fk |