guix-commits
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

branch master updated: gnu: Add emacs-company-coq.


From: guix-commits
Subject: branch master updated: gnu: Add emacs-company-coq.
Date: Mon, 30 Mar 2020 08:37:56 -0400

This is an automated email from the git hooks/post-receive script.

ngz pushed a commit to branch master
in repository guix.

The following commit(s) were added to refs/heads/master by this push:
     new f931d46  gnu: Add emacs-company-coq.
f931d46 is described below

commit f931d46ce3e342f53dee926d3cff70b081f58e5f
Author: John Soo <address@hidden>
AuthorDate: Mon Mar 30 14:36:38 2020 +0200

    gnu: Add emacs-company-coq.
    
    * gnu/packages/emacs-xyz.scm (emacs-company-coq): New variable.
---
 gnu/packages/emacs-xyz.scm | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/gnu/packages/emacs-xyz.scm b/gnu/packages/emacs-xyz.scm
index 05499ab..db5b242 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"))



reply via email to

[Prev in Thread] Current Thread [Next in Thread]