From 60810aaecee193a8e4b8a91f5b8c75b8e7e9941c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 30 Nov 2014 13:39:04 +0100
Subject: Continuing a8ad3abc15a2 which actually forgot to ensure freshness in
 current env.

---
 tactics/evar_tactics.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 311eb657b4..7faede2f2f 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -72,6 +72,7 @@ let let_evar name typ =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let id = Namegen.id_of_name_using_hdchar env typ name in
+    let id = Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) in
     let sigma',evar = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
-- 
cgit v1.2.3