From d9cb4762690826615519c01f9d5bb7cee21e9e09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Jan 2016 17:21:46 +0100
Subject: [PATCH] The tactics setoid_subst x and cofe_subst now also clear x.
---
theories/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index c2190568..85c0fd52 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
--
GitLab