1.2.6 only works in coq-8.12, 1.2.6.1 works from coq 8.12 to coq 8.16

released/packages/coq-pi-agm/coq-pi-agm.1.2.6.1/opam

@@ -0,0 +1,34 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+
+homepage: "http://www-sop.inria.fr/members/Yves.Bertot/"
+bug-reports: "[email protected]"
+license: "CECILL-B"
+build: [["coq_makefile" "-f" "_CoqProject" "-o" "Makefile" ]
+       [ make "-j" "%{jobs}%" ]]
+install: [ make "install" "DEST='%{lib}%/coq/user-contrib/pi_agm'" ]
+depends: [
+  "ocaml"
+  "coq" {>= "8.12" & < "8.17~" }
+  "coq-coquelicot" {>= "3" & < "4~"}
+  "coq-interval" {>= "4"}
+]
+dev-repo: "git+https://github.com/ybertot/pi-agm.git"
+tags: [ "keyword:real analysis" "keyword:pi" "category:Mathematics/Real Calculus and Topology" "logpath:agm" "date:2020-06-23" ]
+authors: [ "Yves Bertot <[email protected]>" ]
+synopsis:
+  "Computing thousands or millions of digits of PI with arithmetic-geometric means"
+description: """
+This is a proof of correctness for two algorithms to compute PI to high
+precision using arithmetic-geometric means.  A first file contains
+the calculus-based proofs for an abstract view of the algorithm, where all
+numbers are real numbers.  A second file describes how to approximate all
+computations using large integers.  Other files describe the second algorithm
+which is close to the one used in mpfr, for instance.
+
+The whole development can be used to produce mathematically proved and
+formally verified approximations of PI."""
+url {
+  src: "https://github.com/ybertot/pi-agm/releases/download/v1.2.6.1/pi-agm-fix.1.2.6.tgz"
+  checksum: "sha256=450657c57d6b9d3d455212e367ac64070062e93cae837be1263acffe0cba68f9"
+}

released/packages/coq-pi-agm/coq-pi-agm.1.2.6/opam

@@ -9,7 +9,7 @@ build: [["coq_makefile" "-f" "_CoqProject" "-o" "Makefile" ]
 install: [ make "install" "DEST='%{lib}%/coq/user-contrib/pi_agm'" ]
 depends: [
   "ocaml"
-  "coq" {>= "8.12" & < "8.17~" }
+  "coq" {>= "8.12" & < "8.13~" }
   "coq-coquelicot" {>= "3" & < "4~"}
   "coq-interval" {>= "4"}
 ]