summaryrefslogtreecommitdiff
path: root/gnu/packages/emacs-xyz.scm
diff options
context:
space:
mode:
Diffstat (limited to 'gnu/packages/emacs-xyz.scm')
-rw-r--r--gnu/packages/emacs-xyz.scm37
1 files changed, 37 insertions, 0 deletions
diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
index 05499aba0b..db5b24220a 100644
--- a/gnu/packages/emacs-xyz.scm
+++ b/gnu/packages/emacs-xyz.scm
@@ -3898,6 +3898,43 @@ completion candidate when using the Company text completion framework.")
@code{company-math}.")
(license license:gpl3+))))
+(define-public emacs-company-coq
+ (package
+ (name "emacs-company-coq")
+ (version "1.0.1")
+ (source
+ (origin
+ (method git-fetch)
+ (uri
+ (git-reference
+ (url "https://github.com/cpitclaudel/company-coq")
+ (commit version)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0dxi4h8xqq5647k7h89s4pi8nwyj3brlhsckrv3p3b1g4dr6mk3b"))))
+ (inputs
+ `(("emacs-company" ,emacs-company)
+ ("emacs-company-math" ,emacs-company-math)
+ ("emacs-dash" ,emacs-dash)
+ ("emacs-yasnippet" ,emacs-yasnippet)))
+ (build-system emacs-build-system)
+ (home-page "https://github.com/cpitclaudel/company-coq")
+ (synopsis "Emacs extensions for Proof General's Coq mode")
+ (description "This package includes a collection of Company mode backends
+for Proof-General's Coq mode, and many useful extensions to Proof-General. It
+features:
+
+@itemize
+@item Prettification of operators, types, and subscripts,
+@item Auto-completion,
+@item Insertion of cases,
+@item Fully explicit intros,
+@item Outlines, code folding, and jumping to definition,
+@item Help with errors,
+@item and more.
+@end itemize")
+ (license license:gpl3+)))
+
(define-public emacs-company-math
(let ((commit "600e49449644f6835f9dc3501bc58461999e8ab9")
(revision "1"))