From 114a77e55db43c5507ed25eb47543f2c8e9199df Mon Sep 17 00:00:00 2001
From: Jean-Pierre De Jesus DIAZ <jean@foundation.xyz>
Date: Tue, 20 Aug 2024 12:31:18 +0200
Subject: [PATCH] gnu: coq: Propagate ocaml-zarith.

Otherwise each Coq plugin needs to specify it.

* gnu/packages/coq.scm (coq)[inputs]: Move ocaml-zarith from here...
[propagated-inptus]: ... to here.
(coq-gappa)[inputs]: Remove ocaml-zarith.
(coq-bignums)[inputs]: Likewise.
(coq-interval)[inputs]: Likewise.
(coq-equations)[inputs]: Likewise.

Change-Id: I63cab11032cc6d4673efc9fdcf14be2929bda05e
Signed-off-by: Zheng Junjie <zhengjunjie@iscas.ac.cn>
---
 gnu/packages/coq.scm | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 4857426613..be95d16991 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -91,8 +91,10 @@ (define-public coq
                      (libdir (string-append out "/lib/ocaml/site-lib")))
                 (invoke "dune" "install" "--prefix" out
                         "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
+    (propagated-inputs
+     (list ocaml-zarith))
     (inputs
-     (list gmp ocaml-zarith))
+     (list gmp))
     (native-inputs
      (list ocaml-ounit2 which))
     (properties '((upstream-name . "coq"))) ; also for inherited packages
@@ -114,7 +116,7 @@ (define-public coq-ide-server
      `(#:tests? #f
        #:package "coqide-server"))
     (inputs
-     (list coq gmp ocaml-zarith))))
+     (list coq gmp))))
 
 (define-public coq-ide
   (package
@@ -319,7 +321,7 @@ (define-public coq-gappa
            bison
            flex))
     (inputs
-     (list gmp mpfr ocaml-zarith boost))
+     (list gmp mpfr boost))
     (propagated-inputs
      (list coq-flocq))
     (arguments
@@ -457,7 +459,7 @@ (define-public coq-bignums
     (native-inputs
      (list ocaml coq))
     (inputs
-     (list camlp5 ocaml-zarith))
+     (list camlp5))
     (arguments
      `(#:tests? #f ; No test target.
        #:make-flags
@@ -495,8 +497,7 @@ (define-public coq-interval
      `(("flocq" ,coq-flocq)
        ("bignums" ,coq-bignums)
        ("coquelicot" ,coq-coquelicot)
-       ("mathcomp" ,coq-mathcomp)
-       ("ocaml-zarith" ,ocaml-zarith)))
+       ("mathcomp" ,coq-mathcomp)))
     (arguments
      `(#:configure-flags
        (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
@@ -579,8 +580,6 @@ (define-public coq-equations
     (build-system gnu-build-system)
     (native-inputs
      (list ocaml coq camlp5))
-    (inputs
-     (list ocaml-zarith))
     (arguments
      `(#:test-target "test-suite"
        #:make-flags (list (string-append "COQLIBINSTALL="