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 ++++++++------
 plugins/ssr/ssrfwd.ml        |  4 +---
 plugins/ssr/ssrtacticals.ml  |  4 +---
 4 files changed, 11 insertions(+), 13 deletions(-)

(limited to 'plugins')

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 =
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index e367cd32d6..f67cf20e49 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -25,9 +25,7 @@ module RelDecl = Context.Rel.Declaration
 (** 8. Forward chaining tactics (pose, set, have, suffice, wlog) *)
 (** Defined identifier *)
 
-
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl Locusops.nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
 
 let ssrposetac (id, (_, t)) gl =
   let ist, t =
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 83581f3416..f12f9fac0f 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
 open Constr
 open Termops
 open Tacmach
-open Locusops
 
 open Ssrast
 open Ssrcommon
@@ -82,8 +81,7 @@ let pf_clauseids gl gens clseq =
 
 let hidden_clseq = function InHyps | InHypsSeq | InAllHyps -> true | _ -> false
 
-let settac id c = Tactics.letin_tac None (Name id) c None
-let posetac id cl = Proofview.V82.of_tactic (settac id cl nowhere)
+let posetac id cl = Proofview.V82.of_tactic (Tactics.pose_tac (Name id) cl)
 
 let hidetacs clseq idhide cl0 =
   if not (hidden_clseq clseq) then  [] else
-- 
cgit v1.2.3