#+title:    :lang coq
#+subtitle: Proofs as programs
#+created:  August 14, 2018
#+since:    21.12.0 (#804)

* Description :unfold:
This module adds [[https://coq.inria.fr][coq]] support, powered by [[https://proofgeneral.github.io][Proof General]].

- Code completion ([[https://github.com/cpitclaudel/company-coq][company-coq]])
- [[https://github.com/hlissner/doom-snippets/tree/master/coq-mode][Snippets]]

** Maintainers
/This module has no dedicated maintainers./ [[doom-contrib-maintainer:][Become a maintainer?]]

** Module flags
/This module has no flags./

** Packages
- [[doom-package:proof-general]]
- [[doom-package:company-coq]]

** Hacks
+ Replaces coq-mode abbrevs with yasnippet snippets from doom's snippet library

** TODO Changelog
# This section will be machine generated. Don't edit it by hand.
/This module does not have a changelog yet./

* Installation
+ [[id:01cffea4-3329-45e2-a892-95a384ab2338][Enable this module in your ~doom!~ block.]]
+ To use the completion features of company-coq you need to enable ~(:completion company)~
+ Make sure you have Coq installed and that the ~coqtop~ command is available. This comes with a standard installation of Coq.
  You can use your linux distribution's Coq package or one of the methods given on the [[https://coq.inria.fr/download][Coq website]].
  
* TODO Usage
#+begin_quote
 󱌣 This module has no usage documentation yet. [[doom-contrib-module:][Write some?]]
#+end_quote

* Configuration
This module provides no additional configuration over that of the [[Packages]] it loads

* Troubleshooting
See [[https://github.com/hlissner/doom-emacs/issues?q=is%3Aissue+is%3Aopen+label%3A%22%3Alang+coq"][related github issues]]
/There are no known problems with this module./ [[doom-report:][Report one?]]

* Frequently asked questions
/This module has no FAQs yet./ [[doom-suggest-faq:][Ask one?]]

* TODO Appendix
#+begin_quote
 󱌣 This module has no appendix yet. [[doom-contrib-module:][Write one?]]
#+end_quote