The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Coq-Club,

It's a great pleasure to announce the first release of company-coq 
(https://github.com/cpitclaudel/company-coq/), a collection of extensions for 
Proof General [1]. 

Company-Coq builds on top of Proof General to make proof-writing more 
efficient and more enjoyable. At its core are a collection of autocompletion 
engines, offering suggestions and documentation as you type tactics, 
commands, module names, and Ltac constructs. Company-Coq comes with a 
collection of snippets, an enhanced display of mathematics, documentation for 
Coq errors, code folding, automatic extraction of lemmas, inline 
documentation popups (quick peek), enhanced support for CoqDoc comments, 
notifications for long-running proofs, and source browsing features.

Installing company-coq is very easy: I encourage you to try it out (setup 
instructions are on the GitHub page), to suggest features and report issues, 
and to enjoy the improved experience. And if you are coming to CoqPL this 
year, please attend our presentation [2] and join us for discussion on the 
future of Coq development environments!

[1] Aspinall, D. (2000). Proof General: A generic tool for proof development. 
In Tools and Algorithms for the Construction and Analysis of Systems (pp. 
38-43). Springer Berlin Heidelberg.
[2] Pit-Claudel, C. & Courtieu, P. (2016). Company-Coq: Taking Proof General 
one step closer to a real IDE. In CoqPL'16: The Second International Workshop 
on Coq for PL.

Attachment: signature.asc
Description: OpenPGP digital signature