Coquelicot 3.4.5.

released/packages/coq-coquelicot/coq-coquelicot.3.4.5/opam

@@ -0,0 +1,38 @@
+opam-version: "2.0"
+maintainer: "guillaume.melquiond@inria.fr"
+homepage: "http://coquelicot.saclay.inria.fr/"
+dev-repo: "git+https://gitlab.inria.fr/coquelicot/coquelicot.git"
+bug-reports: "https://gitlab.inria.fr/coquelicot/coquelicot/issues"
+license: "LGPL-3.0-or-later"
+build: [
+  ["autoconf"] {dev}
+  ["./configure"]
+  ["./remake" "-j%{jobs}%"]
+]
+install: ["./remake" "install"]
+depends: [
+  ("coq" {>= "8.12" & < "8.17~"} | ("coq-core" & ("coq-stdlib" | "rocq-stdlib")))
+  "coq-mathcomp-ssreflect" {>= "1.6"}
+  "conf-autoconf" {build & dev}
+  "ocaml" {build}
+  ("conf-g++" {build} | "conf-clang" {build})
+]
+tags: [
+  "keyword:real analysis"
+  "keyword:topology"
+  "keyword:filters"
+  "keyword:metric spaces"
+  "category:Mathematics/Real Calculus and Topology"
+  "logpath:Coquelicot"
+  "date:2026-08-27"
+]
+authors: [
+  "Sylvie Boldo <sylvie.boldo@inria.fr>"
+  "Catherine Lelay <catherine.lelay@inria.fr>"
+  "Guillaume Melquiond <guillaume.melquiond@inria.fr>"
+]
+synopsis: "A Coq formalization of real analysis compatible with the standard library"
+url {
+  src: "https://coquelicot.gitlabpages.inria.fr/releases/coquelicot-3.4.5.tar.gz"
+  checksum: "sha512=6a94f674715175347ff9938f8ac0f6e865c0019e6b6317d292e4c9d7e30df7ebd41dfe48205a61f66c0bde0da1702d9831161439189dbc8337524d51f05e1a99"
+}