diff options
Diffstat (limited to 'src/tac2stdlib.ml')
| -rw-r--r-- | src/tac2stdlib.ml | 11 |
1 files changed, 11 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 |