From 8a8fd265158fa3fe7eea65b50c3da722e81fa688 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 14:43:30 +0200
Subject: Binding more primitive tactics.

---
 theories/Std.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'theories')

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".
-- 
cgit v1.2.3