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.

2 files changed, 30 insertions, 0 deletions

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