From c53fb4be8c65a89dd03d4aedc2fc65d9807da915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Sep 2017 00:15:09 +0200
Subject: Binding the pose/set family of tactics.

---
 src/tac2stdlib.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'src/tac2stdlib.ml')

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 28bcd6a1cf..0db71fb293 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -294,13 +294,12 @@ let () = define_prim2 "tac_pose" begin fun idopt c ->
   Tactics.letin_tac None na c None Locusops.nowhere
 end
 
-let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
+let () = define_prim3 "tac_set" begin fun ev p cl ->
   let ev = Value.to_bool ev in
-  let na = to_name idopt in
   let cl = to_clause cl in
   Proofview.tclEVARMAP >>= fun sigma ->
-  thaw c >>= fun c ->
-  let c = Value.to_constr c in
+  thaw p >>= fun p ->
+  let (na, c) = to_pair to_name Value.to_constr p in
   Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
-- 
cgit v1.2.3