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: | en_US |
| Published: |
2016
|
| Online Access: | http://hdl.handle.net/1721.1/101149 https://orcid.org/0000-0002-1900-3901 |