summaryrefslogtreecommitdiff
path: root/gnu/packages/coq.scm
diff options
context:
space:
mode:
authorBrett Gilio <brettg@gnu.org>2020-01-06 01:34:23 -0600
committerBrett Gilio <brettg@gnu.org>2020-01-06 21:03:21 -0600
commita5727da96aa131604fe1552b8938e3a2998b2745 (patch)
treeb805d037da588a56e39eae0cef1ee36515643065 /gnu/packages/coq.scm
parent1ac40045029aacc2d360f4bd24d716c1306a54e8 (diff)
downloadguix-patches-a5727da96aa131604fe1552b8938e3a2998b2745.tar
guix-patches-a5727da96aa131604fe1552b8938e3a2998b2745.tar.gz
gnu: coq: Reword several comments.
* gnu/packages/coq.scm (coq): Reword several comments to improve readability.
Diffstat (limited to 'gnu/packages/coq.scm')
-rw-r--r--gnu/packages/coq.scm10
1 files changed, 5 insertions, 5 deletions
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 45aaa83711..89b1c2149b 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -95,8 +95,8 @@
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
(bin (string-append out "/bin")))
- ;; These are exact copies of the version without the .opt suffix.
- ;; Remove them to save 35 MiB in the result
+ ;; These files are exact copies without `.opt` extension.
+ ;; Removing these saves 35 MiB in the resulting package.
(delete-file (string-append bin "/coqtop.opt"))
(delete-file (string-append bin "/coqidetop.opt")))
#t))
@@ -112,9 +112,9 @@
(lambda _
(with-directory-excursion "test-suite"
;; These two tests fail.
- ;; This one fails because the output is not formatted as expected.
+ ;; Fails because the output is not formatted as expected.
(delete-file-recursively "coq-makefile/timing")
- ;; This one fails because we didn't build coqtop.byte.
+ ;; Fails because we didn't build coqtop.byte.
(delete-file-recursively "coq-makefile/findlib-package")
(invoke "make")))))))
(home-page "https://coq.inria.fr")
@@ -123,7 +123,7 @@
"Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal specification.
It is developed using Objective Caml and Camlp5.")
- ;; The code is distributed under lgpl2.1.
+ ;; The source code is distributed under lgpl2.1.
;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+))))