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...
Main Authors: | , |
---|---|
Other Authors: | , , |
Format: | Article |
Language: | English |
Published: |
2021-09-23T17:56:26Z.
|
Subjects: | |
Online Access: | Get fulltext |