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

(limited to 'plugins/ssr')

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