~ruther/guix-local

189501bf3b8facced98f08e73b7cdb83ec7a272b — Julien Lepiller 4 years ago bcd4c7a
gnu: proof-general: Update to latest commit.

* gnu/packages/coq.scm (proof-general): Update to latest commit.
[license]: Change to glp3+.
1 files changed, 5 insertions(+), 5 deletions(-)

M gnu/packages/coq.scm
M gnu/packages/coq.scm => gnu/packages/coq.scm +5 -5
@@ 119,9 119,9 @@ It is developed using Objective Caml and Camlp5.")
(define-public proof-general
  ;; The latest release is from 2016 and there has been more than 450 commits
  ;; since then.
  ;; Commit from 2021-06-07.
  (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a")
        (revision "0"))
  ;; Commit from 2021-11-25.
  (let ((commit "1b1083e86e0cddc20ff2f1a6b25c7a7eee2edf02")
        (revision "1"))
    (package
      (name "proof-general")
      (version (git-version "4.4" revision commit))


@@ 133,7 133,7 @@ It is developed using Objective Caml and Camlp5.")
                (file-name (git-file-name name version))
                (sha256
                 (base32
                  "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
                  "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j"))))
      (build-system gnu-build-system)
      (native-inputs
       `(("emacs" ,emacs-minimal)


@@ 201,7 201,7 @@ It is developed using Objective Caml and Camlp5.")
       "Proof General is a major mode to turn Emacs into an interactive proof
assistant to write formal mathematical proofs using a variety of theorem
provers.")
      (license license:gpl2+))))
      (license license:gpl3+))))

(define-public coq-flocq
  (package