This package includes a collection of company-mode backends for
Proof-General's Coq mode, and many useful extensions to Proof-General.

See https://github.com/cpitclaudel/company-coq/ for a detailed description,
including screenshots and documentation.  After installing, you may want to
use M-x company-coq-tutorial to open the tutorial.