Adding new notations.

2 files changed, 28 insertions, 0 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index d0400667db..ec7a6b0b12 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -35,3 +35,29 @@ Ltac2 Notation "constructor" n(tactic) bnd(thunk(bindings)) :=
 Ltac2 Notation "econstructor" := Std.econstructor ().
 Ltac2 Notation "econstructor" n(tactic) bnd(bindings) :=
   Std.econstructor_n n bnd.
+
+Ltac2 eelim c bnd use :=
+    let use := match use with
+    | None => None
+    | Some u =>
+      let ((_, c, wth)) := u in Some (c, wth)
+    end in
+  Std.eelim (c, bnd) use.
+
+Ltac2 elim c bnd use :=
+  Control.with_holes
+    (fun () => c (), bnd (), use ())
+    (fun ((c, bnd, use)) =>
+      let use := match use with
+      | None => None
+      | Some u =>
+        let ((_, c, wth)) := u in Some (c, wth)
+      end in
+    Std.elim (c, bnd) use).
+
+Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
+  use(thunk(opt(seq("using", constr, bindings)))) := elim c bnd use.
+
+Ltac2 Notation "eelim" c(constr) bnd(bindings)
+  use(opt(seq("using", constr, bindings))) :=
+  eelim c bnd use.
diff --git a/theories/Std.v b/theories/Std.v
index d2b85f215e..3d0f463c5e 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -78,7 +78,9 @@ with or_and_intro_pattern := [
 Ltac2 @ external intros : intro_pattern list -> unit := "ltac2" "tac_intros".
 Ltac2 @ external eintros : intro_pattern list -> unit := "ltac2" "tac_eintros".
 
+Ltac2 @ external elim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_elim".
 Ltac2 @ external eelim : constr_with_bindings -> constr_with_bindings option -> unit := "ltac2" "tac_eelim".
+Ltac2 @ external case : constr_with_bindings -> unit := "ltac2" "tac_case".
 Ltac2 @ external ecase : constr_with_bindings -> unit := "ltac2" "tac_ecase".
 
 Ltac2 @ external egeneralize : (constr * occurrences * ident option) list -> unit := "ltac2" "tac_egeneralize".