(define-public coq-coquelicot

  (package

    (name "coq-coquelicot")

    (version "3.0.0")

    (source (origin

              (method url-fetch)

              (uri (string-append "https://gforge.inria.fr/frs/download.php/"

                                  "file/36537/coquelicot-" version ".tar.gz"))

              (sha256

               (base32

                "0fx99bvsbdizj00gx2im8939y4wwl05f4qhw184j90kcx5vjxxv9"))))

    (build-system gnu-build-system)

    (native-inputs

     `(("ocaml" ,ocaml)

       ("which" ,which)

       ("coq" ,coq-fix)))

    (propagated-inputs

     `(("mathcomp" ,coq-mathcomp)))

    (arguments

     `(#:configure-flags

       (list (string-append "--libdir=" (assoc-ref %outputs "out")

                            "/lib/coq/user-contrib/Coquelicot"))

       #:phases

       (modify-phases %standard-phases

         (add-before 'configure 'fix-remake

           (lambda _

             (substitute* "remake.cpp"

               (("/bin/sh") (which "sh")))))

         (replace 'build

           (lambda _

             (zero? (system* "./remake"))))

         (replace 'check

           (lambda _

             (zero? (system* "./remake" "check"))))

         (replace 'install

           (lambda _

             (zero? (system* "./remake" "install")))))))

    (home-page "http://coquelicot.saclay.inria.fr/index.html")

    (synopsis "Coq library for Reals")

    (description "Coquelicot is an easier way of writing formulas and theorem

statements, achieved by relying on total functions in place of dependent types

for limits, derivatives, integrals, power series, and so on.  To help with the

proof process, the library comes with a comprehensive set of theorems that cover

not only these notions, but also some extensions such as parametric integrals,

two-dimensional differentiability, asymptotic behaviors.  It also offers some

automations for performing differentiability proofs.  Moreover, Coquelicot is a

conservative extension of Coq's standard library and provides correspondence

theorems between the two libraries.")

    (license license:lgpl3+)))

       ("coq" ,coq-fix)))

       ("coquelicot" ,coq-coquelicot)

(define-public coq-fix

  (package

    (inherit coq)

    (name "coq-fix")

    (native-search-paths

      (list (search-path-specification

              (variable "COQPATH")

              (files (list "lib/coq/user-contrib")))))))