From 2f2c7200c9dd6b2f008989a98cc9a35df8c37300 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Aug 2020 11:20:29 +0200
Subject: tacinterp mini cleanup useless letin

---
 plugins/ltac/tacinterp.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2ca9a0e69d..88480194c8 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2125,8 +2125,7 @@ let _ =
     (* EJGA: We should also pass the proof name if desired, for now
        poly seems like enough to get reasonable behavior in practice
      *)
-    let name, poly = Id.of_string "ltac_gen", poly in
-    let name, poly = Id.of_string "ltac_gen", poly in
+    let name = Id.of_string "ltac_gen" in
     let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
-- 
cgit v1.2.3