Merge pull request #3356 from affeldt-aist/monae.0.9.0

release monae 0.9.0

Author: palmskog

released/packages/coq-monae/coq-monae.0.9.0/opam

@@ -0,0 +1,51 @@
+opam-version: "2.0"
+maintainer: "Reynald Affeldt <[email protected]>"
+
+homepage: "https://github.com/affeldt-aist/monae"
+dev-repo: "git+https://github.com/affeldt-aist/monae.git"
+bug-reports: "https://github.com/affeldt-aist/monae/issues"
+license: "LGPL-2.1-or-later"
+
+synopsis: "Monads and equational reasoning in Coq"
+description: """
+This Coq library contains a hierarchy of monads with their laws used
+in several examples of monadic equational reasoning."""
+
+build: [make "-j%{jobs}%" ]
+install: [make "install_full"]
+depends: [
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.3.0") }
+  "coq-mathcomp-fingroup" { (>= "2.3.0") }
+  "coq-mathcomp-algebra" { (>= "2.3.0") }
+  "coq-mathcomp-solvable" { (>= "2.3.0") }
+  "coq-mathcomp-field" { (>= "2.3.0") }
+  "coq-mathcomp-analysis" { (>= "1.9.0") }
+  "coq-infotheo" { >= "0.9.1"}
+  "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
+  "coq-hierarchy-builder" { >= "1.7.0" }
+  "coq-equations" { >= "1.3" & < "1.4~" }
+]
+
+tags: [
+  "keyword:monae"
+  "keyword:effects"
+  "keyword:probability"
+  "keyword:nondeterminism"
+  "logpath:monae.theories"
+  "logpath:monaeImpredicativeSet"
+  "date: 2025-02-26"
+]
+authors: [
+  "Reynald Affeldt"
+  "David Nowak"
+  "Takafumi Saikawa"
+  "Jacques Garrigue"
+  "Ayumu Saito"
+  "Celestine Sauvage"
+  "Kazunari Tanaka"
+]
+url {
+  src: "https://github.com/affeldt-aist/monae/archive/0.9.0.tar.gz"
+  checksum: "sha512=aa7ac3fd5fec110cf17ec1f054ff23d3f7ccbbd82a29fece0d18000c2829fc84746580c3229c9aaa633ca9d0338824823826af2a34494774d2374999f6bcb19b"
+}