Company-Coq: Taking Proof General one step closer to a real IDE

Company-Coq is a new Emacs package that extends Proof General with a contextual auto-completion engine for Coq proofs and many additional facilities to make writing proofs easier and more efficient. Beyond fuzzy auto-completion of tactics, options, module names, and local definitions, company-coq of...

Full description

Bibliographic Details
Main Authors: Pit-Claudel, Clement F. (Contributor), Courtieu, Pierre (Author)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: 2016-02-09T20:37:06Z.
Subjects:
Online Access:Get fulltext