From 0f45543718e9b02a86114876998b2f884dd883b4 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 6 Nov 2023 11:36:11 +0100 Subject: [PATCH] Interval 4.9.0 --- .../coq-interval/coq-interval.4.9.0/opam | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 released/packages/coq-interval/coq-interval.4.9.0/opam diff --git a/released/packages/coq-interval/coq-interval.4.9.0/opam b/released/packages/coq-interval/coq-interval.4.9.0/opam new file mode 100644 index 000000000..e77114b0a --- /dev/null +++ b/released/packages/coq-interval/coq-interval.4.9.0/opam @@ -0,0 +1,43 @@ +opam-version: "2.0" +maintainer: "guillaume.melquiond@inria.fr" +homepage: "https://coqinterval.gitlabpages.inria.fr/" +dev-repo: "git+https://gitlab.inria.fr/coqinterval/interval.git" +bug-reports: "https://gitlab.inria.fr/coqinterval/interval/issues" +license: "CeCILL-C" +build: [ + ["autoconf"] {dev} + ["./configure"] + ["./remake" "-j%{jobs}%"] +] +install: ["./remake" "install"] +depends: [ + "coq" {>= "8.11"} + "coq-bignums" + "coq-flocq" {>= "3.1"} + "coq-mathcomp-ssreflect" {>= "1.6"} + "coq-coquelicot" {>= "3.0"} + "conf-autoconf" {build & dev} + ("conf-g++" {build} | "conf-clang" {build}) +] +tags: [ + "keyword:interval arithmetic" + "keyword:decision procedure" + "keyword:floating-point arithmetic" + "keyword:reflexive tactic" + "keyword:Taylor models" + "category:Mathematics/Real Calculus and Topology" + "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures" + "logpath:Interval" + "date:2023-11-06" +] +authors: [ + "Guillaume Melquiond " + "Érik Martin-Dorel " + "Pierre Roux " + "Thomas Sibut-Pinote " +] +synopsis: "A Coq tactic for proving bounds on real-valued expressions automatically" +url { + src: "https://coqinterval.gitlabpages.inria.fr/releases/interval-4.9.0.tar.gz" + checksum: "sha512=256e7d4780a8116d62bf89aaf5dfbe3b861d1f37ab35f52b1267ca8f8bf735cb173a6beb5568ad84057eb9fa5fb7437219a68d876093d37790984b2ed21ac5d3" +}