From a903429392e96dad8ed404b079367dea05232150 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.

---
 modures/logic.v   | 6 +++---
 prelude/tactics.v | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/modures/logic.v b/modures/logic.v
index 64ffb9f7f..1b377b722 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -134,9 +134,9 @@ Next Obligation.
   assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
   { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using @ra_included_l.
     apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
-  exists x1, x2'; split_ands; [done| |].
-  * cofe_subst y; apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
-  * cofe_subst y; apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
+  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
+  * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
+  * apply uPred_weaken with x2 n1; eauto using cmra_valid_op_r.
 Qed.
 
 Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
diff --git a/prelude/tactics.v b/prelude/tactics.v
index c2190568d..85c0fd52a 100644
--- a/prelude/tactics.v
+++ b/prelude/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