More bindings to primitive tactics.

2 files changed, 42 insertions, 1 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index d2c7059985..2d52904faf 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -130,6 +130,23 @@ Ltac2 Notation split := split.
 Ltac2 Notation "esplit" bnd(thunk(bindings)) := split0 true bnd.
 Ltac2 Notation esplit := esplit.
 
+Ltac2 exists0 ev bnds := match bnds with
+| [] => split0 ev (fun () => Std.NoBindings)
+| _ =>
+  let rec aux bnds := match bnds with
+  | [] => ()
+  | bnd :: bnds => split0 ev bnd; aux bnds
+  end in
+  aux bnds
+end.
+
+(*
+Ltac2 Notation "exists" bnd(list0(thunk(bindings), ",")) := exists0 false bnd.
+
+Ltac2 Notation "eexists" bnd(list0(thunk(bindings), ",")) := exists0 true bnd.
+Ltac2 Notation eexists := eexists.
+*)
+
 Ltac2 left0 ev bnd := enter_h ev Std.left bnd.
 
 Ltac2 Notation "left" bnd(thunk(bindings)) := left0 false bnd.
@@ -316,7 +333,7 @@ Ltac2 Notation "erewrite"
   tac(opt(seq("by", thunk(tactic)))) :=
   rewrite0 true rw cl tac.
 
-(** Other base tactics *)
+(** coretactics *)
 
 Ltac2 Notation reflexivity := Std.reflexivity ().
 
@@ -329,3 +346,17 @@ Ltac2 Notation admit := Std.admit ().
 Ltac2 Notation clear := Std.keep [].
 
 Ltac2 Notation refine := Control.refine.
+
+(** extratactics *)
+
+Ltac2 absurd0 c := Control.enter (fun _ => Std.absurd (c ())).
+
+Ltac2 Notation absurd := absurd0.
+
+Ltac2 subst0 ids := match ids with
+| [] => Std.subst_all ()
+| _ => Std.subst ids
+end.
+
+Ltac2 Notation "subst" ids(list0(ident)) := subst0 ids.
+Ltac2 Notation subst := subst.
diff --git a/theories/Std.v b/theories/Std.v
index dd81835c40..f380c10af8 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -184,7 +184,17 @@ 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".
 
+(** coretactics *)
+
+(** extratactics *)
+
+Ltac2 @ external discriminate : evar_flag -> destruction_arg option -> unit := "ltac2" "tac_discriminate".
+Ltac2 @ external injection : evar_flag -> intro_pattern list option -> destruction_arg option -> unit := "ltac2" "tac_injection".
+
 Ltac2 @ external absurd : constr -> unit := "ltac2" "tac_absurd".
+Ltac2 @ external contradiction : constr_with_bindings option -> unit := "ltac2" "tac_contradiction".
+
+Ltac2 @ external autorewrite : bool -> (unit -> unit) option -> ident list -> clause -> unit := "ltac2" "tac_autorewrite".
 
 Ltac2 @ external subst : ident list -> unit := "ltac2" "tac_subst".
 Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall".