6 files changed, 120 insertions, 1 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index e0a65dde2d..fef16dcc06 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -325,7 +325,7 @@ let prm_constr_kind : ml_tactic = function
     |])
   | Const (cst, u) ->
     ValBlk (10, [|
-      Value.of_ext Value.val_constant cst;
+      Value.of_constant cst;
       of_instance sigma u;
     |])
   | Ind (ind, u) ->
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 74e2b02aeb..49b49d92fd 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -122,3 +122,6 @@ let of_array f vl = ValBlk (0, Array.map f vl)
 let to_array f = function
 | ValBlk (0, vl) -> Array.map f vl
 | _ -> assert false
+
+let of_constant c = of_ext val_constant c
+let to_constant c = to_ext val_constant c
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 3f429995ce..b69ca9a382 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -59,6 +59,9 @@ val to_pattern : valexpr -> Pattern.constr_pattern
 val of_pp : Pp.t -> valexpr
 val to_pp : valexpr -> Pp.t
 
+val of_constant : Constant.t -> valexpr
+val to_constant : valexpr -> Constant.t
+
 val of_ext : 'a Val.typ -> 'a -> valexpr
 val to_ext : 'a Val.typ -> valexpr -> 'a
 
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 7c7b539113..e093b5c97f 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -9,6 +9,7 @@
 open Names
 open Locus
 open Misctypes
+open Genredexpr
 open Tac2expr
 open Tac2core
 open Proofview.Notations
@@ -66,6 +67,24 @@ let to_clause = function
   { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
 | _ -> assert false
 
+let to_evaluable_ref = function
+| ValBlk (0, [| id |]) -> EvalVarRef (Value.to_ident id)
+| ValBlk (1, [| cst |]) -> EvalConstRef (Value.to_constant cst)
+| _ -> assert false
+
+let to_red_flag = function
+| ValBlk (0, [| beta; iota; fix; cofix; zeta; delta; const |]) ->
+  {
+    rBeta = Value.to_bool beta;
+    rMatch = Value.to_bool iota;
+    rFix = Value.to_bool fix;
+    rCofix = Value.to_bool cofix;
+    rZeta = Value.to_bool zeta;
+    rDelta = Value.to_bool delta;
+    rConst = Value.to_list to_evaluable_ref const;
+  }
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -81,6 +100,8 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
+let thaw f = Tac2interp.interp_app f [v_unit]
+
 let define_prim0 name tac =
   let tac = function
   | [_] -> lift tac
@@ -102,6 +123,13 @@ let define_prim2 name tac =
   in
   Tac2env.define_primitive (pname name) tac
 
+let define_prim3 name tac =
+  let tac = function
+  | [x; y; z] -> lift (tac x y z)
+  | _ -> assert false
+  in
+  Tac2env.define_primitive (pname name) tac
+
 (** Tactics from Tacexpr *)
 
 let () = define_prim2 "tac_eelim" begin fun c copt ->
@@ -125,6 +153,58 @@ let () = define_prim1 "tac_egeneralize" begin fun cl ->
   Tactics.new_generalize_gen cl
 end
 
+let () = define_prim2 "tac_pose" begin fun idopt c ->
+  let na = to_name idopt in
+  let c = Value.to_constr c in
+  Tactics.letin_tac None na c None Locusops.nowhere
+end
+
+let () = define_prim3 "tac_set" begin fun idopt c cl ->
+  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
+  Tactics.letin_pat_tac false None na (sigma, c) cl
+end
+
+let () = define_prim3 "tac_eset" begin fun idopt c cl ->
+  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
+  Tactics.letin_pat_tac true None na (sigma, c) cl
+end
+
+let () = define_prim1 "tac_red" begin fun cl ->
+  let cl = to_clause cl in
+  Tactics.reduce (Red false) cl
+end
+
+let () = define_prim1 "tac_hnf" begin fun cl ->
+  let cl = to_clause cl in
+  Tactics.reduce Hnf cl
+end
+
+let () = define_prim2 "tac_cbv" begin fun flags cl ->
+  let flags = to_red_flag flags in
+  let cl = to_clause cl in
+  Tactics.reduce (Cbv flags) cl
+end
+
+let () = define_prim2 "tac_cbn" begin fun flags cl ->
+  let flags = to_red_flag flags in
+  let cl = to_clause cl in
+  Tactics.reduce (Cbn flags) cl
+end
+
+let () = define_prim2 "tac_lazy" begin fun flags cl ->
+  let flags = to_red_flag flags in
+  let cl = to_clause cl in
+  Tactics.reduce (Lazy flags) cl
+end
+
 (** Tactics from coretactics *)
 
 let () = define_prim0 "tac_reflexivity" Tactics.intros_reflexivity
diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index ece6fca06a..6b30d42c09 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -143,3 +143,11 @@ Ltac2 rec do n tac := match Int.equal n 0 with
 end.
 
 Print Ltac2 do.
+
+Goal forall x, 1 + x = x + 1.
+Proof.
+refine (fun () => '(fun x => _)).
+Std.cbv {
+  Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
+  Std.rZeta := true; Std.rDelta := false; rConst := [];
+} { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
diff --git a/theories/Std.v b/theories/Std.v
index a9eced6cbb..3070c2e005 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -34,6 +34,21 @@ Ltac2 Type clause := {
   on_concl : occurrences;
 }.
 
+Ltac2 Type evaluable_reference := [
+| EvalVarRef (ident)
+| EvalConstRef (constant)
+].
+
+Ltac2 Type red_flags := {
+  rBeta : bool;
+  rMatch : bool;
+  rFix : bool;
+  rCofix : bool;
+  rZeta : bool;
+  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+  rConst : evaluable_reference list
+}.
+
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
 Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim".
@@ -41,6 +56,16 @@ Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".
 
 Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize".
 
+Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
+Ltac2 @ external set : ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
+Ltac2 @ external eset : ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_eset".
+
+Ltac2 @ external red : clause -> unit := "ltac2" "tac_red".
+Ltac2 @ external hnf : clause -> unit := "ltac2" "tac_hnf".
+Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv".
+Ltac2 @ external cbn : red_flags -> clause -> unit := "ltac2" "tac_cbn".
+Ltac2 @ external lazy : red_flags -> clause -> unit := "ltac2" "tac_lazy".
+
 Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity".
 
 Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption".