Sniper is a Coq plugin which provides a two steps general automation tactic called snipe. The first step consists of a modular combination of small certifying pre-processing transformations. Each of them transforms a Coq goal in order to generate first-order statements. Then, the new generated goal is solved automatically by the second step, which calls external SMT solvers. In the current implementation of snipe, we deal with algebraic datatypes, uninterpreted functions, prenex polymorphism and different representations of logic and integers. In this talk, we will present the general methodology of snipe and we will detail the transformation it uses.