From faf40da077f20a67a45fe98f8ef99f90440ef16d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 16:32:10 +0200
Subject: Adding new notations.

---
 src/tac2stdlib.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/tac2stdlib.ml')

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
-- 
cgit v1.2.3