Get Gentoo!
gentoo.org sites
gentoo.org Wiki Bugs Forums Packages
Planet Archives Sources
Infra Status

app-emacs/
company-coq

Collection of extensions for Proof General's Coq mode

https://github.com/cpitclaudel/company-coq/

Available Versions

Version amd64 x86 alpha arm arm64 hppa ia64 ppc ppc64 riscv sparc
1.0.1_p20220314 : 0 ~amd64 ~x86 alpha arm arm64 hppa ia64 ppc ppc64 riscv sparc
1.0.1_p20210708-r1 : 0 ~amd64 ~x86 alpha arm arm64 hppa ia64 ppc ppc64 riscv sparc

Package Metadata

  • Upstream
    Bugs-To https://github.com/cpitclaudel/company-coq/issues/
    Remote-Id https://github.com/cpitclaudel/company-coq
  • Full description
    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.
  • License
    GPL-3+
  • Maintainer(s)
    Gentoo GNU Emacs project