From 1fda28c317a2394aa3ee84e0e680e878333c8782 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 19 May 2016 13:01:19 +0200 Subject: 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. --- theories/Classes/Morphisms.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Classes') 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 -- cgit v1.2.3