From 5fcbb0eb7b624ee18b817e7fd1b3b0d2fbc9bd35 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 13 Aug 2018 19:47:37 +0200
Subject: Less crazy implementation of the "pose" family of tactics.

The previous implementation was calling a lot of useless unification
even though the net effect of the tactic was simply to add a binding to
the environment.

Interestingly the base tactic was used in several higher level tactics,
including evar and ssreflect pose.

Part of the fix for #8245.
---
 plugins/ltac/evar_tactics.ml |  2 +-
 plugins/ltac/tacinterp.ml    | 14 ++++++++------
 2 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 84f13d2131..73490a2dfd 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -94,7 +94,7 @@ let let_evar name typ =
     in
     let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
+    (Tactics.pose_tac (Name.Name id) evar)
   end
   
 let hget_evar n =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a0446bd6a0..124974b6e3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1664,16 +1664,18 @@ and interp_atomic ist tac : unit Proofview.tactic =
         (* We try to fully-typecheck the term *)
           let flags = open_constr_use_classes_flags () in
           let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
-          let let_tac b na c cl eqpat =
-            let id = Option.default (make IntroAnonymous) eqpat in
-            let with_eq = if b then None else Some (true,id) in
-            Tactics.letin_tac with_eq na c None cl
-          in
           let na = interp_name ist env sigma na in
+          let let_tac =
+            if b then Tactics.pose_tac na c_interp
+            else
+              let id = Option.default (make IntroAnonymous) eqpat in
+              let with_eq = Some (true, id) in
+              Tactics.letin_tac with_eq na c_interp None Locusops.nowhere
+          in
           Tacticals.New.tclWITHHOLES ev
           (name_atomic ~env
             (TacLetTac(ev,na,c_interp,clp,b,eqpat))
-            (let_tac b na c_interp clp eqpat)) sigma
+            let_tac) sigma
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
-- 
cgit v1.2.3