Binding move and intro.

3 files changed, 29 insertions, 0 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 03141805ef..1762952e55 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -176,6 +176,13 @@ let to_inversion_kind = function
 | ValInt 2 -> Misctypes.FullInversionClear
 | _ -> assert false
 
+let to_move_location = function
+| ValInt 0 -> MoveFirst
+| ValInt 1 -> MoveLast
+| ValBlk (0, [|id|]) -> MoveAfter (Value.to_ident id)
+| ValBlk (1, [|id|]) -> MoveBefore (Value.to_ident id)
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -488,6 +495,19 @@ end
 
 let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
 
+let () = define_prim2 "tac_move" begin fun _ id mv ->
+  let id = Value.to_ident id in
+  let mv = to_move_location mv in
+  Tactics.move_hyp id mv
+end
+
+let () = define_prim2 "tac_intro" begin fun _ id mv ->
+  let id = Value.to_option Value.to_ident id in
+  let mv = Value.to_option to_move_location mv in
+  let mv = Option.default MoveLast mv in
+  Tactics.intro_move id mv
+end
+
 (*
 
 TACTIC EXTEND exact
diff --git a/theories/Notations.v b/theories/Notations.v
index 8a3e769d12..9ecca018af 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -399,6 +399,11 @@ Ltac2 exact0 ev c :=
 Ltac2 Notation "exact" c(thunk(open_constr)) := exact0 false c.
 Ltac2 Notation "eexact" c(thunk(open_constr)) := exact0 true c.
 
+Ltac2 Notation "intro" id(opt(ident)) mv(opt(move_location)) := Std.intro id mv.
+Ltac2 Notation intro := intro.
+
+Ltac2 Notation "move" id(ident) mv(move_location) := Std.move id mv.
+
 Ltac2 Notation reflexivity := Std.reflexivity ().
 
 Ltac2 symmetry0 cl :=
diff --git a/theories/Std.v b/theories/Std.v
index 3f98bdbaab..a937560b10 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -214,6 +214,10 @@ Ltac2 @ external inversion : inversion_kind -> destruction_arg -> intro_pattern
 
 (** coretactics *)
 
+Ltac2 @ external move : ident -> move_location -> unit := "ltac2" "tac_move".
+
+Ltac2 @ external intro : ident option -> move_location option -> unit := "ltac2" "tac_intro".
+
 (** extratactics *)
 
 Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "ltac2" "tac_discriminate".