company-coq
Collection of extensions for Proof General's Coq mode
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 offers offline in-editor documentation, convenient snippets, and multiple other Coq-specific IDE features.
homepage ↗ github: cpitclaudel/company-coq
Available in
| Overlay | Newest | Ebuilds | Last activity | |
|---|---|---|---|---|
| gentoo gitweb ↗ | 1.0.1_p20220314 | 1 | 13 h | details › |
| melpa GitHub ↗ | 20260223.1721 | 1 | 20 h | details › |
| melpa-stable GitHub ↗ | 1.0.1 | 1 | 20 h | details › |