Exporting some basic tactics from Ltac1.

2 files changed, 60 insertions, 0 deletions

diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index 221f7be424..4cd3fafcb2 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -14,3 +14,4 @@ Require Ltac2.Array.
 Require Ltac2.Message.
 Require Ltac2.Constr.
 Require Ltac2.Control.
+Require Ltac2.Std.
diff --git a/theories/Std.v b/theories/Std.v
new file mode 100644
index 0000000000..5cc1622ba9
--- /dev/null
+++ b/theories/Std.v
@@ -0,0 +1,59 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+(** Standard, built-in tactics. See Ltac1 for documentation. *)
+
+Ltac2 @ external reflexivity : unit -> unit := "ltac2" "tac_reflexivity".
+
+Ltac2 @ external assumption : unit -> unit := "ltac2" "tac_assumption".
+
+Ltac2 @ external transitivity : constr -> unit := "ltac2" "tac_transitivity".
+
+Ltac2 @ external etransitivity : unit -> unit := "ltac2" "tac_etransitivity".
+
+Ltac2 @ external cut : constr -> unit := "ltac2" "tac_cut".
+
+Ltac2 @ external left : unit -> unit := "ltac2" "tac_left".
+Ltac2 @ external eleft : unit -> unit := "ltac2" "tac_eleft".
+Ltac2 @ external right : unit -> unit := "ltac2" "tac_right".
+Ltac2 @ external eright : unit -> unit := "ltac2" "tac_eright".
+
+Ltac2 @ external constructor : unit -> unit := "ltac2" "tac_constructor".
+Ltac2 @ external econstructor : unit -> unit := "ltac2" "tac_econstructor".
+Ltac2 @ external split : unit -> unit := "ltac2" "tac_split".
+Ltac2 @ external esplit : unit -> unit := "ltac2" "tac_esplit".
+
+Ltac2 @ external constructor_n : int -> unit := "ltac2" "tac_constructorn".
+Ltac2 @ external econstructor_n : int -> unit := "ltac2" "tac_econstructorn".
+
+Ltac2 @ external symmetry : unit -> unit := "ltac2" "tac_symmetry".
+
+Ltac2 @ external rename : (ident * ident) list -> unit := "ltac2" "tac_rename".
+
+Ltac2 @ external revert : ident list -> unit := "ltac2" "tac_revert".
+
+Ltac2 @ external admit : unit -> unit := "ltac2" "tac_admit".
+
+Ltac2 @ external fix_ : ident option -> int -> unit := "ltac2" "tac_fix".
+Ltac2 @ external cofix_ : ident option -> unit := "ltac2" "tac_cofix".
+
+Ltac2 @ external clear : ident list -> unit := "ltac2" "tac_clear".
+Ltac2 @ external keep : ident list -> unit := "ltac2" "tac_keep".
+
+Ltac2 @ external clearbody : ident list -> unit := "ltac2" "tac_clearbody".
+
+Ltac2 @ external exact_no_check : constr -> unit := "ltac2" "tac_exactnocheck".
+Ltac2 @ external vm_cast_no_check : constr -> unit := "ltac2" "tac_vmcastnocheck".
+Ltac2 @ external native_cast_no_check : constr -> unit := "ltac2" "tac_nativecastnocheck".
+
+Ltac2 @ external absurd : constr -> unit := "ltac2" "tac_absurd".
+
+Ltac2 @ external subst : ident list -> unit := "ltac2" "tac_subst".
+Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall".