Used an evar name based on the local def name in "evar" tactic.

1 files changed, 3 insertions, 2 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index b569ef97fd..311eb657b4 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,7 +71,8 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let sigma',evar = Evarutil.new_evar env sigma ~src typ in
+    let id = Namegen.id_of_name_using_hdchar env typ name 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 name evar None Locusops.nowhere)
+      (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
   end