Hello, John Soo writes: > Company-coq is indispensable when working in coq for me. I slightly expounded the description and applied your patch as f931d46ce3e342f53dee926d3cff70b081f58e5f. Thank you! Regards, -- Nicolas Goaziou