Binding the pose/set family of tactics.

11 files changed, 85 insertions, 12 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 7295f31181..dfd586d5ef 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -40,6 +40,27 @@ let test_lpar_idnum_coloneq =
               | _ -> err ())
         | _ -> err ())
 
+(* Hack to recognize "(x := t)" and "($x := t)" *)
+let test_lpar_coloneq =
+  Gram.Entry.of_parser "test_coloneq"
+    (fun strm ->
+      match stream_nth 0 strm with
+        | KEYWORD "(" ->
+            (match stream_nth 1 strm with
+              | IDENT _ ->
+                  (match stream_nth 2 strm with
+                    | KEYWORD ":=" -> ()
+                    | _ -> err ())
+              | KEYWORD "$" ->
+                (match stream_nth 2 strm with
+                  | IDENT _ ->
+                      (match stream_nth 3 strm with
+                        | KEYWORD ":=" -> ()
+                        | _ -> err ())
+                  | _ -> err ())
+              | _ -> err ())
+        | _ -> err ())
+
 (* Hack to recognize "(x)" *)
 let test_lpar_id_rpar =
   Gram.Entry.of_parser "lpar_id_coloneq"
@@ -369,7 +390,7 @@ GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
           q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
           q_destruction_arg q_reference q_with_bindings q_constr_matching
-          q_hintdb q_move_location;
+          q_hintdb q_move_location q_pose;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -702,6 +723,20 @@ GEXTEND Gram
   q_move_location:
     [ [ mv = move_location -> mv ] ]
   ;
+  as_name:
+    [ [ -> None
+      | "as"; id = ident_or_anti -> Some id
+    ] ]
+  ;
+  pose:
+    [ [ test_lpar_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
+        Loc.tag ~loc:!@loc (Some id, c)
+      | c = Constr.constr; na = as_name -> Loc.tag ~loc:!@loc (na, c)
+    ] ]
+  ;
+  q_pose:
+    [ [ p = pose -> p ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7bd0164b4d..bb6578090d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1118,6 +1118,7 @@ let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
 let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
 let () = add_expr_scope "reference" q_reference Tac2quote.of_reference
 let () = add_expr_scope "move_location" q_move_location Tac2quote.of_move_location
+let () = add_expr_scope "pose" q_pose Tac2quote.of_pose
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Tac2quote.wit_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 26f96f7d72..d622aaba69 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -40,6 +40,7 @@ let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
 let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
 let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
 let q_move_location = Pcoq.Gram.entry_create "tactic:q_move_location"
+let q_pose = Pcoq.Gram.entry_create "tactic:q_pose"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 7c71130402..55e658884b 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -79,6 +79,7 @@ val q_strategy_flag : strategy_flag Pcoq.Gram.entry
 val q_constr_matching : constr_matching Pcoq.Gram.entry
 val q_hintdb : hintdb Pcoq.Gram.entry
 val q_move_location : move_location Pcoq.Gram.entry
+val q_pose : pose Pcoq.Gram.entry
 end
 
 (** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 7d02022e07..580039afe5 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -139,3 +139,5 @@ type move_location_r =
 | QMoveLast
 
 type move_location = move_location_r located
+
+type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index f14612d58f..466c1f5094 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -370,3 +370,6 @@ let of_move_location (loc, mv) = match mv with
 | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id]
 | QMoveFirst -> std_constructor ?loc "MoveFirst" []
 | QMoveLast -> std_constructor ?loc "MoveLast" []
+
+let of_pose p =
+  of_pair (fun id -> of_option (fun id -> of_anti of_ident id) id) of_open_constr p
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 9f42c60042..ccb832535a 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -75,6 +75,8 @@ val of_dispatch : dispatch -> raw_tacexpr
 
 val of_strategy_flag : strategy_flag -> raw_tacexpr
 
+val of_pose : pose -> raw_tacexpr
+
 val of_constr_matching : constr_matching -> raw_tacexpr
 
 (** {5 Generic arguments} *)
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
 
diff --git a/tests/example2.v b/tests/example2.v
index a7eb02050b..b667e19bbd 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -208,3 +208,17 @@ Proof.
 refine '(let x := 0 in _).
 eexists; exists &x; reflexivity.
 Qed.
+
+Goal True.
+Proof.
+pose (X := True).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+let x := @foo in
+set ($x := True) in * |-.
+constructor.
+Qed.
+
diff --git a/theories/Notations.v b/theories/Notations.v
index 9b2b04f9e6..65b05113ae 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -270,6 +270,27 @@ Ltac2 Notation "apply"
   cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
   apply0 true false cb cl.
 
+Ltac2 default_on_concl cl :=
+match cl with
+| None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
+| Some cl => cl
+end.
+
+Ltac2 pose0 ev p :=
+  enter_h ev (fun ev ((na, p)) => Std.pose na p) p.
+
+Ltac2 Notation "pose" p(thunk(pose)) :=
+  pose0 false p.
+
+Ltac2 Notation "epose" p(thunk(pose)) :=
+  pose0 true p.
+
+Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) :=
+  Std.set false p (default_on_concl cl).
+
+Ltac2 Notation "eset" p(thunk(pose)) cl(opt(clause)) :=
+  Std.set true p (default_on_concl cl).
+
 Ltac2 induction0 ev ic use :=
   let f ev use := Std.induction ev ic use in
   enter_h ev f use.
@@ -323,12 +344,6 @@ Ltac2 Notation "inversion_clear"
   ids(opt(seq("in", list1(ident)))) :=
   Std.inversion Std.FullInversionClear arg pat ids.
 
-Ltac2 default_on_concl cl :=
-match cl with
-| None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
-| Some cl => cl
-end.
-
 Ltac2 Notation "red" cl(opt(clause)) :=
   Std.red (default_on_concl cl).
 Ltac2 Notation red := red.
diff --git a/theories/Std.v b/theories/Std.v
index f8b269dce6..42bd9edde0 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -135,7 +135,7 @@ Ltac2 @ external assert : constr -> (unit -> unit) option option -> intro_patter
 Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_pattern option -> unit := "ltac2" "tac_enough".
 
 Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
-Ltac2 @ external set : evar_flag -> ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
+Ltac2 @ external set : evar_flag -> (unit -> ident option * constr) -> clause -> unit := "ltac2" "tac_set".
 
 Ltac2 @ external destruct : evar_flag -> induction_clause list ->
   constr_with_bindings option -> unit := "ltac2" "tac_induction".