Binding move and intro.

1 files changed, 20 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