Commit d9cb4762 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

The tactics setoid_subst x and cofe_subst now also clear x.

parent 42f4c16a
...@@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x := ...@@ -218,7 +218,7 @@ Ltac setoid_subst_aux R x :=
try match H' with H => fail 2 end; try match H' with H => fail 2 end;
setoid_rewrite H in H' setoid_rewrite H in H'
end; end;
clear H clear x H
end. end.
Ltac setoid_subst := Ltac setoid_subst :=
repeat match goal with repeat match goal with
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment