aboutsummaryrefslogtreecommitdiff
path: root/gnu
diff options
context:
space:
mode:
Diffstat (limited to 'gnu')
-rw-r--r--gnu/packages/ocaml.scm46
1 files changed, 46 insertions, 0 deletions
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm
index 86af187aa0..43bbdcd6e2 100644
--- a/gnu/packages/ocaml.scm
+++ b/gnu/packages/ocaml.scm
@@ -3345,3 +3345,49 @@ 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+)))
+
+(define-public coq-interval
+ (package
+ (name "coq-interval")
+ (version "3.2.0")
+ (source (origin
+ (method url-fetch)
+ (uri (string-append "https://gforge.inria.fr/frs/download.php/"
+ "file/36538/interval-" version ".tar.gz"))
+ (sha256
+ (base32
+ "16ir7mizl18kwa1ls8fwjih6r87894bvc1r6lh85cd43la7nriq3"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("ocaml" ,ocaml)
+ ("which" ,which)
+ ("coq" ,coq)))
+ (propagated-inputs
+ `(("flocq" ,coq-flocq)
+ ("coquelicot" ,coq-coquelicot)
+ ("mathcomp" ,coq-mathcomp)))
+ (arguments
+ `(#:configure-flags
+ (list (string-append "--libdir=" (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib/Gappa"))
+ #: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://coq-interval.gforge.inria.fr/")
+ (synopsis "Coq tactics to simplify inequality proofs")
+ (description "Interval provides vernacular files containing tactics for
+simplifying the proofs of inequalities on expressions of real numbers for the
+Coq proof assistant.")
+ (license license:cecill-c)))