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.