From 90cbf2a05e221b9920646faa1f61b341f32327cf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Aug 2016 15:00:06 +0200
Subject: [PATCH] Clear temporary hypotheses created by iIntoEntails.

---
 proofmode/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c878fa56e..404eb149b 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -224,7 +224,7 @@ Tactic Notation "iIntoEntails" open_constr(t) :=
     | True ⊢ _ => apply t
     | _ ⊢ _ => apply (uPred.entails_wand _ _ t)
     | _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t)
-    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H)]
+    | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H); clear H]
     | ∀ _ : ?T, _ =>
        (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
        (* This is a workarround for Coq bug #4969. *)
-- 
GitLab