From 8394619baceb118df92e355377fd543bb1aa501a Mon Sep 17 00:00:00 2001
From: Ludovic Courtès <ludo@gnu.org>
Date: Mon, 13 Dec 2021 17:18:24 +0100
Subject: gnu: Simplify package inputs.

This commit was obtained by running:

  ./pre-inst-env guix style

without any additional argument.
---
 gnu/packages/coq.scm | 90 +++++++++++++++++-----------------------------------
 1 file changed, 29 insertions(+), 61 deletions(-)

(limited to 'gnu/packages/coq.scm')

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index cf0c67f214..5173726ec2 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -78,11 +78,9 @@
             (separator #f))))
     (build-system dune-build-system)
     (inputs
-     `(("gmp" ,gmp)
-       ("ocaml-zarith" ,ocaml-zarith)))
+     (list gmp ocaml-zarith))
     (native-inputs
-     `(("ocaml-ounit2" ,ocaml-ounit2)
-       ("which" ,which)))
+     (list ocaml-ounit2 which))
     (arguments
      `(#:package "coq-core"
        #:test-target "."))
@@ -105,9 +103,7 @@ It is developed using Objective Caml and Camlp5.")
      `(#:package "coq-stdlib"
        #:test-target "."))
     (inputs
-     `(("coq-core" ,coq-core)
-       ("gmp" ,gmp)
-       ("ocaml-zarith" ,ocaml-zarith)))
+     (list coq-core gmp ocaml-zarith))
     (native-inputs '())))
 
 (define-public coq
@@ -118,8 +114,7 @@ It is developed using Objective Caml and Camlp5.")
      `(#:package "coq"
        #:test-target "."))
     (propagated-inputs
-     `(("coq-core" ,coq-core)
-       ("coq-stdlib" ,coq-stdlib)))
+     (list coq-core coq-stdlib))
     (native-inputs '())))
 
 (define-public coq-ide-server
@@ -130,9 +125,7 @@ It is developed using Objective Caml and Camlp5.")
      `(#:tests? #f
        #:package "coqide-server"))
     (inputs
-     `(("coq" ,coq)
-       ("gmp" ,gmp)
-       ("ocaml-zarith" ,ocaml-zarith)))))
+     (list coq gmp ocaml-zarith))))
 
 (define-public coq-ide
   (package
@@ -142,8 +135,7 @@ It is developed using Objective Caml and Camlp5.")
      `(#:tests? #f
        #:package "coqide"))
     (propagated-inputs
-     `(("coq" ,coq)
-       ("coq-ide-server" ,coq-ide-server)))
+     (list coq coq-ide-server))
     (inputs
      `(("lablgtk3" ,lablgtk3)))))
 
@@ -170,7 +162,7 @@ It is developed using Objective Caml and Camlp5.")
        `(("emacs" ,emacs-minimal)
          ("texinfo" ,texinfo)))
       (inputs
-       `(("perl" ,perl)))
+       (list perl))
       (arguments
        (let ((base-directory "/share/emacs/site-lisp/ProofGeneral"))
          `(#:tests? #f                  ; no check target
@@ -250,11 +242,7 @@ provers.")
          "0j7vq7ifqcdaj2x881aha2rl51l2p72y1cn7r2xya0fjgsssfigy"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("autoconf" ,autoconf)
-       ("automake" ,automake)
-       ("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     (list autoconf automake ocaml which coq))
     (arguments
      `(#:configure-flags
        (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
@@ -301,21 +289,18 @@ inside Coq.")
          "1ivh8xm1c8191rm4riamjzya2x6ls96qax5byir1fywf9hbxr1vg"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("autoconf" ,autoconf)
-       ("automake" ,automake)
-       ("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)
-       ("camlp5" ,camlp5)
-       ("bison" ,bison)
-       ("flex" ,flex)))
+     (list autoconf
+           automake
+           ocaml
+           which
+           coq
+           camlp5
+           bison
+           flex))
     (inputs
-     `(("gmp" ,gmp)
-       ("mpfr" ,mpfr)
-       ("ocaml-zarith" ,ocaml-zarith)
-       ("boost" ,boost)))
+     (list gmp mpfr ocaml-zarith boost))
     (propagated-inputs
-     `(("coq-flocq" ,coq-flocq)))
+     (list coq-flocq))
     (arguments
      `(#:configure-flags
        (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
@@ -361,9 +346,7 @@ assistant.")
         (base32 "0aj8hsdzzds5w0p1858s2b6k9zssjcxa6kgpi0q1nvaml4zfpkcc"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     (list ocaml which coq))
     (arguments
      `(#:tests? #f ; No tests.
        #:make-flags (list (string-append "COQLIBINSTALL="
@@ -401,11 +384,7 @@ part of the distribution.")
          "146s5y2xsc7wb43m1pq1n4p14hw99gqbzx0ic3a4naxq16v7cv4w"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("autoconf" ,autoconf)
-       ("automake" ,automake)
-       ("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     (list autoconf automake ocaml which coq))
     (propagated-inputs
      `(("mathcomp" ,coq-mathcomp)))
     (arguments
@@ -453,11 +432,9 @@ theorems between the two libraries.")
                 "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml" ,ocaml)
-       ("coq" ,coq)))
+     (list ocaml coq))
     (inputs
-     `(("camlp5" ,camlp5)
-       ("ocaml-zarith" ,ocaml-zarith)))
+     (list camlp5 ocaml-zarith))
     (arguments
      `(#:tests? #f ; No test target.
        #:make-flags
@@ -488,11 +465,7 @@ provides BigN, BigZ, BigQ that used to be part of Coq standard library.")
          "0sr9psildc0sda07r2r47rfgyry49yklk38bg04yyvry5j5pryb6"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("autoconf" ,autoconf)
-       ("automake" ,automake)
-       ("ocaml" ,ocaml)
-       ("which" ,which)
-       ("coq" ,coq)))
+     (list autoconf automake ocaml which coq))
     (propagated-inputs
      `(("flocq" ,coq-flocq)
        ("bignums" ,coq-bignums)
@@ -549,7 +522,7 @@ Coq proof assistant.")
          (modify-phases %standard-phases
            (delete 'configure))))
       (native-inputs
-       `(("coq" ,coq)))
+       (list coq))
       (home-page "https://www.ps.uni-saarland.de/autosubst/")
       (synopsis "Coq library for parallel de Bruijn substitutions")
       (description "Formalizing syntactic theories with variable binders is
@@ -580,11 +553,9 @@ uses Ltac to synthesize the substitution operation.")
                 "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("ocaml"  ,ocaml)
-       ("coq"    ,coq)
-       ("camlp5" ,camlp5)))
+     (list ocaml coq camlp5))
     (inputs
-     `(("ocaml-zarith" ,ocaml-zarith)))
+     (list ocaml-zarith))
     (arguments
      `(#:test-target "test-suite"
        #:make-flags (list (string-append "COQLIBINSTALL="
@@ -625,12 +596,9 @@ kernel.")
           "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac"))))
     (build-system gnu-build-system)
     (native-inputs
-     `(("coq" ,coq)
-       ("ocaml" ,ocaml)
-       ("ocamlbuild" ,ocamlbuild)
-       ("ocaml-findlib" ,ocaml-findlib)))
+     (list coq ocaml ocamlbuild ocaml-findlib))
     (inputs
-     `(("ocaml-num" ,ocaml-num)))
+     (list ocaml-num))
     (arguments
      `(#:tests? #f                      ;included in Makefile
        #:make-flags (list (string-append "COQLIBINSTALL="
@@ -670,7 +638,7 @@ also provided in Coq, without associated proofs.")
                 "1l1w6srzydjg0h3f4krrfgvz455h56shyy2lbcnwdbzjkahibl7v"))))
     (build-system gnu-build-system)
     (inputs
-     `(("coq" ,coq)))
+     (list coq))
     (arguments
      `(#:tests? #f ; Tests are executed during build phase.
        #:make-flags (list (string-append "COQLIBINSTALL="
-- 
cgit v1.2.3