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.

6 files changed, 41 insertions, 13 deletions

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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a8ebe08ca..ac07c8e2c9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2690,6 +2690,34 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
       (sigma, mkNamedLetIn id c t x)
 
+let pose_tac na c =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    let hyps = named_context_val env in
+    let concl = Proofview.Goal.concl gl in
+    let t = typ_of env sigma c in
+    let (sigma, t) = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in
+    let id = match na with
+    | Name id ->
+      let () = if mem_named_context_val id hyps then
+        user_err (str "Variable " ++ Id.print id ++ str " is already declared.")
+      in
+      id
+    | Anonymous ->
+      let id = id_of_name_using_hdchar env sigma t Anonymous in
+      next_ident_away_in_goal id (ids_of_named_context_val hyps)
+    in
+    Proofview.Unsafe.tclEVARS sigma <*>
+    Refine.refine ~typecheck:false begin fun sigma ->
+      let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
+      let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
+      let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in
+      let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in
+      (sigma, mkLetIn (Name id, c, t, body))
+    end
+  end
+
 let letin_tac with_eq id c ty occs =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 57f20d2ff2..c088e404b0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -390,6 +390,8 @@ val cut        : types -> unit Proofview.tactic
 
 (** {6 Tactics for adding local definitions. } *)
 
+val pose_tac : Name.t -> constr -> unit Proofview.tactic
+
 val letin_tac : (bool * intro_pattern_naming) option ->
   Name.t -> constr -> types option -> clause -> unit Proofview.tactic