  Recently, we developed an automated theorem prover for projective incidence
geometry. This prover, based on a combinatorial approach using matroids,
proceeds by saturation using the matroid rules. It is designed as an
independent tool, implemented in C, which takes a geometric configuration as
input and produces as output some Coq proof scripts: the statement of the
expected theorem, a proof script proving the theorem and possibly some
auxiliary lemmas. In this document, we show how to embed such an external tool
as a plugin in Coq so that it can be used as a simple tactic.
