Tentatively implementing apply.

2 files changed, 34 insertions, 5 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index 2d7b4c8a8b..1bc48d587a 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -37,11 +37,11 @@ Ltac2 Notation "econstructor" n(tactic) bnd(bindings) :=
   Std.constructor_n true n bnd.
 
 Ltac2 elim0 ev c bnd use :=
-    let use := match use with
-    | None => None
-    | Some u =>
-      let ((_, c, wth)) := u in Some (c, wth)
-    end in
+  let use := match use with
+  | None => None
+  | Some u =>
+    let ((_, c, wth)) := u in Some (c, wth)
+  end in
   Std.elim ev (c, bnd) use.
 
 Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
@@ -53,3 +53,28 @@ Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
 Ltac2 Notation "eelim" c(constr) bnd(bindings)
   use(opt(seq("using", constr, bindings))) :=
   elim0 true c bnd use.
+
+Ltac2 apply0 adv ev cb cl :=
+  let cl := match cl with
+  | None => None
+  | Some p =>
+    let ((_, id, ipat)) := p in
+    let p := match ipat with
+    | None => None
+    | Some p =>
+      let ((_, ipat)) := p in
+      Some ipat
+    end in
+    Some (id, p)
+  end in
+  Std.apply adv ev cb cl.
+
+Ltac2 Notation "eapply"
+  cb(list1(thunk(seq(constr, bindings)), ","))
+  cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
+  apply0 true true cb cl.
+
+Ltac2 Notation "apply"
+  cb(list1(thunk(seq(constr, bindings)), ","))
+  cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
+  apply0 true false cb cl.
diff --git a/theories/Std.v b/theories/Std.v
index 20504f1247..3d1e8f462d 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -74,11 +74,15 @@ with or_and_intro_pattern := [
 ].
 
 Ltac2 Type evar_flag := bool.
+Ltac2 Type advanced_flag := bool.
 
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
 Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "ltac2" "tac_intros".
 
+Ltac2 @ external apply : advanced_flag -> evar_flag ->
+  (unit -> constr_with_bindings) list -> (ident * (intro_pattern option)) option -> unit := "ltac2" "tac_apply".
+
 Ltac2 @ external elim : evar_flag -> constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim".
 Ltac2 @ external case : evar_flag -> constr_with_bindings -> unit := "ltac2" "tac_case".