diff --git a/theories/tactics.v b/theories/tactics.v index c2190568d733add0f43597a64b05d57d01df5563..85c0fd52a54257bc9ffbad52eb355ea039478895 100644 --- a/theories/tactics.v +++ b/theories/tactics.v @@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x := try match H' with H => fail 2 end; setoid_rewrite H in H' end; - clear H + clear x H end. Ltac setoid_subst := repeat match goal with