diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-19 13:01:19 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 1fda28c317a2394aa3ee84e0e680e878333c8782 (patch) | |
| tree | 1f87845554f8bba09e4d77d5a6ccd1a8e1b80e01 /theories | |
| parent | 46388674943195e5d64340d54553c98d5698a68e (diff) | |
setoid_rewrite: fix the Params resolution tactic
Add a substitution of a local variable by its body to
ensure proper unification without having to make all local
variables unfoldable.
Diffstat (limited to 'theories')
| -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 |