4 files changed, 129 insertions, 11 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index f28c5c5dcf..515cadc525 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -557,6 +557,14 @@ let prm_refine : ml_tactic = function
   end >>= fun () -> return v_unit
 | _ -> assert false
 
+let prm_with_holes : ml_tactic = function
+| [x; f] ->
+  Proofview.tclEVARMAP >>= fun sigma0 ->
+  thaw x >>= fun ans ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
+  Tacticals.New.tclWITHHOLES false (interp_app f [ans]) sigma
+| _ -> assert false
 
 (** Registering *)
 
@@ -615,6 +623,7 @@ let () = Tac2env.define_primitive (pname "goal") prm_goal
 let () = Tac2env.define_primitive (pname "hyp") prm_hyp
 let () = Tac2env.define_primitive (pname "hyps") prm_hyps
 let () = Tac2env.define_primitive (pname "refine") prm_refine
+let () = Tac2env.define_primitive (pname "with_holes") prm_with_holes
 
 (** ML types *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 2094898ced..a75500eae7 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -239,6 +239,9 @@ let interp_ml_object t = MLType.obj t
 let coq_prefix =
   MPfile (DirPath.make (List.map Id.of_string ["Init"; "Ltac2"]))
 
+let std_prefix =
+  MPfile (DirPath.make (List.map Id.of_string ["Std"; "Ltac2"]))
+
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2"
diff --git a/src/tac2env.mli b/src/tac2env.mli
index e26109b691..fea03c4285 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -106,6 +106,9 @@ val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object
 val coq_prefix : ModPath.t
 (** Path where primitive datatypes are defined in Ltac2 plugin. *)
 
+val std_prefix : ModPath.t
+(** Path where Ltac-specific datatypes are defined in Ltac2 plugin. *)
+
 (** {5 Generic arguments} *)
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 0aeccbd9c6..7c7b539113 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Locus
 open Misctypes
 open Tac2expr
@@ -14,6 +15,57 @@ open Proofview.Notations
 
 module Value = Tac2ffi
 
+let to_pair f g = function
+| ValBlk (0, [| x; y |]) -> (f x, g y)
+| _ -> assert false
+
+let to_name c = match Value.to_option Value.to_ident c with
+| None -> Anonymous
+| Some id -> Name id
+
+let to_qhyp = function
+| ValBlk (0, [| i |]) -> AnonHyp (Value.to_int i)
+| ValBlk (1, [| id |]) -> NamedHyp (Value.to_ident id)
+| _ -> assert false
+
+let to_bindings = function
+| ValInt 0 -> NoBindings
+| ValBlk (0, [| vl |]) ->
+  ImplicitBindings (Value.to_list Value.to_constr vl)
+| ValBlk (1, [| vl |]) ->
+  ExplicitBindings ((Value.to_list (fun p -> None, to_pair to_qhyp Value.to_constr p) vl))
+| _ -> assert false
+
+let to_constr_with_bindings = function
+| ValBlk (0, [| c; bnd |]) -> (Value.to_constr c, to_bindings bnd)
+| _ -> assert false
+
+let to_int_or_var i = ArgArg (Value.to_int i)
+
+let to_occurrences f = function
+| ValInt 0 -> AllOccurrences
+| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list f vl)
+| ValInt 1 -> NoOccurrences
+| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list f vl)
+| _ -> assert false
+
+let to_hyp_location_flag = function
+| ValInt 0 -> InHyp
+| ValInt 1 -> InHypTypeOnly
+| ValInt 2 -> InHypValueOnly
+| _ -> assert false
+
+let to_clause = function
+| ValBlk (0, [| hyps; concl |]) ->
+  let cast = function
+  | ValBlk (0, [| hyp; occ; flag |]) ->
+    ((to_occurrences to_int_or_var occ, Value.to_ident hyp), to_hyp_location_flag flag)
+  | _ -> assert false
+  in
+  let hyps = Value.to_option (fun h -> Value.to_list cast h) hyps in
+  { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -50,6 +102,29 @@ let define_prim2 name tac =
   in
   Tac2env.define_primitive (pname name) tac
 
+(** Tactics from Tacexpr *)
+
+let () = define_prim2 "tac_eelim" begin fun c copt ->
+  let c = to_constr_with_bindings c in
+  let copt = Value.to_option to_constr_with_bindings copt in
+  Tactics.elim true None c copt
+end
+
+let () = define_prim1 "tac_ecase" begin fun c ->
+  let c = to_constr_with_bindings c in
+  Tactics.general_case_analysis true None c
+end
+
+let () = define_prim1 "tac_egeneralize" begin fun cl ->
+  let cast = function
+  | ValBlk (0, [| c; occs; na |]) ->
+    ((to_occurrences Value.to_int c, Value.to_constr c), to_name na)
+  | _ -> assert false
+  in
+  let cl = Value.to_list cast cl in
+  Tactics.new_generalize_gen cl
+end
+
 (** Tactics from coretactics *)
 
 let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
@@ -76,10 +151,26 @@ let () = define_prim1 "tac_cut" begin fun c ->
   Tactics.cut c
 end
 
-let () = define_prim0 "tac_left" (Tactics.left_with_bindings false NoBindings)
-let () = define_prim0 "tac_eleft" (Tactics.left_with_bindings true NoBindings)
-let () = define_prim0 "tac_right" (Tactics.right_with_bindings false NoBindings)
-let () = define_prim0 "tac_eright" (Tactics.right_with_bindings true NoBindings)
+let () = define_prim1 "tac_left" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.left_with_bindings false bnd
+end
+let () = define_prim1 "tac_eleft" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.left_with_bindings true bnd
+end
+let () = define_prim1 "tac_right" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.right_with_bindings false bnd
+end
+let () = define_prim1 "tac_eright" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.right_with_bindings true bnd
+end
+
+let () = define_prim1 "tac_introsuntil" begin fun h ->
+  Tactics.intros_until (to_qhyp h)
+end
 
 let () = define_prim1 "tac_exactnocheck" begin fun c ->
   Tactics.exact_no_check (Value.to_constr c)
@@ -96,20 +187,32 @@ end
 let () = define_prim0 "tac_constructor" (Tactics.any_constructor false None)
 let () = define_prim0 "tac_econstructor" (Tactics.any_constructor true None)
 
-let () = define_prim1 "tac_constructorn" begin fun n ->
+let () = define_prim2 "tac_constructorn" begin fun n bnd ->
   let n = Value.to_int n in
-  Tactics.constructor_tac false None n NoBindings
+  let bnd = to_bindings bnd in
+  Tactics.constructor_tac false None n bnd
 end
 
-let () = define_prim1 "tac_econstructorn" begin fun n ->
+let () = define_prim2 "tac_econstructorn" begin fun n bnd ->
   let n = Value.to_int n in
-  Tactics.constructor_tac true None n NoBindings
+  let bnd = to_bindings bnd in
+  Tactics.constructor_tac true None n bnd
 end
 
-let () = define_prim0 "tac_symmetry" (Tactics.intros_symmetry Locusops.onConcl)
+let () = define_prim1 "tac_symmetry" begin fun cl ->
+  let cl = to_clause cl in
+  Tactics.intros_symmetry cl
+end
 
-let () = define_prim0 "tac_split" (Tactics.split_with_bindings false [NoBindings])
-let () = define_prim0 "tac_esplit" (Tactics.split_with_bindings true [NoBindings])
+let () = define_prim1 "tac_split" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.split_with_bindings false [bnd]
+end
+
+let () = define_prim1 "tac_esplit" begin fun bnd ->
+  let bnd = to_bindings bnd in
+  Tactics.split_with_bindings true [bnd]
+end
 
 let () = define_prim1 "tac_rename" begin fun ids ->
   let map c = match Value.to_tuple c with