aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-05-19 13:01:19 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-16 18:21:08 +0200
commit1fda28c317a2394aa3ee84e0e680e878333c8782 (patch)
tree1f87845554f8bba09e4d77d5a6ccd1a8e1b80e01 /theories
parent46388674943195e5d64340d54553c98d5698a68e (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.v2
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