  In the context of interactive theorem provers based on a dependent type
theory, automation tactics (dedicated decision procedures, call of automated
solvers, ...) are often limited to goals which are exactly in some expected
logical fragment. This very often prevents users from applying these tactics in
other contexts, even similar ones.
  This paper discusses the design and the implementation of pre-processing
operations for automating formal proofs in the Coq proof assistant. It presents
the implementation of a wide variety of predictible, atomic goal
transformations, which can be composed in various ways to target different
backends. A gallery of examples illustrates how it helps to expand
significantly the power of automation engines.
