Adding new notations.

3 files changed, 39 insertions, 0 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 5c8337d41a..ac530f5130 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -175,12 +175,23 @@ let () = define_prim1 "tac_eintros" begin fun ipat ->
   Tactics.intros_patterns true ipat
 end
 
+let () = define_prim2 "tac_elim" begin fun c copt ->
+  let c = to_constr_with_bindings c in
+  let copt = Value.to_option to_constr_with_bindings copt in
+  Tactics.elim false None c copt
+end
+
 let () = define_prim2 "tac_eelim" begin fun c copt ->
   let c = to_constr_with_bindings c in
   let copt = Value.to_option to_constr_with_bindings copt in
   Tactics.elim true None c copt
 end
 
+let () = define_prim1 "tac_case" begin fun c ->
+  let c = to_constr_with_bindings c in
+  Tactics.general_case_analysis false None c
+end
+
 let () = define_prim1 "tac_ecase" begin fun c ->
   let c = to_constr_with_bindings c in
   Tactics.general_case_analysis true None c
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".