company-coq is a company back-end that offers documentation and keywords autocompletion when editing Coq proof scripts.