Replace rat_of_positive with rat_of_Z

coq-community · Apr 25, 2022 · 84b5e9d · 84b5e9d
1 parent 8449081
commit 84b5e9d
Show file tree

Hide file tree

Showing 6 changed files with 219 additions and 228 deletions.
diff --git a/README.md b/README.md
@@ -48,7 +48,7 @@ remains the sole trusted code base.
   - [CoqEAL 1.0.5 or later](https://github.com/coq-community/coqeal)
   - [MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed)
   - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
-  - [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
+  - [Mczify](https://github.com/math-comp/mczify) 1.2.0 or later
   - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 0.2.0 or later
 - Coq namespace: `mathcomp.apery`
 - Related publication(s):

diff --git a/coq-mathcomp-apery.opam b/coq-mathcomp-apery.opam
@@ -30,7 +30,7 @@ depends: [
   "coq-coqeal" {>= "1.0.5"}
   "coq-mathcomp-real-closed" {>= "1.1.2"}
   "coq-mathcomp-bigenough" {>= "1.0.0"}
-  "coq-mathcomp-zify" {(>= "1.1.0") | (= "dev")}
+  "coq-mathcomp-zify" {(>= "1.2.0") | (= "dev")}
   "coq-mathcomp-algebra-tactics" {(>= "0.2.0") | (= "dev")}
 ]
 

diff --git a/meta.yml b/meta.yml
@@ -98,9 +98,9 @@ dependencies:
     [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
 - opam:
     name: coq-mathcomp-zify
-    version: '{(>= "1.1.0") | (= "dev")}'
+    version: '{(>= "1.2.0") | (= "dev")}'
   description: |-
-    [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
+    [Mczify](https://github.com/math-comp/mczify) 1.2.0 or later
 - opam:
     name: coq-mathcomp-algebra-tactics
     version: '{(>= "0.2.0") | (= "dev")}'