Bump MathComp version to >= 1.12.0 (#3)

* Bump MathComp version to 1.12.0

* Cleanup

.github/workflows/docker-action.yml

@@ -0,0 +1,44 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.11'
+          - 'mathcomp/mathcomp-dev:coq-8.12'
+          - 'mathcomp/mathcomp-dev:coq-8.13'
+          - 'mathcomp/mathcomp-dev:coq-8.14'
+          - 'mathcomp/mathcomp-dev:coq-dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-mathcomp-apery.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -1,9 +1,13 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # Apery
 
-[![CI][action-shield]][action-link]
+[![Docker CI][docker-action-shield]][docker-action-link]
 
-[action-shield]: https://github.com/math-comp/apery/workflows/CI/badge.svg?branch=master
-[action-link]: https://github.com/math-comp/apery/actions?query=workflow%3ACI
+[docker-action-shield]: https://github.com/math-comp/apery/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/apery/actions?query=workflow:"Docker%20CI"
 
 
 
@@ -23,13 +27,13 @@ remains the sole trusted code base.
   - Assia Mahboubi (initial)
   - Thomas Sibut-Pinote (initial)
 - License: [CeCILL-C](Licence_CeCILL-C_V1-en.txt)
-- Compatible Coq versions: 8.11
+- Compatible Coq versions: 8.11 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.10](https://math-comp.github.io)
+  - [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
-  - [CoqEAL 1.0.3 or later](https://github.com/CoqEAL/CoqEAL)
-  - [MathComp real closed fields 1.0.4 or later](https://github.com/math-comp/real-closed)
+  - [CoqEAL 1.0.5 or later](https://github.com/CoqEAL/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)
 - Coq namespace: `mathcomp.apery`
 - Related publication(s):

coq-mathcomp-apery.opam

@@ -1,3 +1,6 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "dev"
@@ -17,15 +20,15 @@ computer algebra program (in this case in Maple/Algolib). These
 relations are formally checked a posteriori, so that Coq's kernel
 remains the sole trusted code base."""
 
-build: [make "-j%{jobs}%" ]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.11" & < "8.12~"}
-  "coq-mathcomp-ssreflect" {>= "1.10" & < "1.11~"}
+  "coq" {(>= "8.11" & < "8.15~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.12" & < "1.14~") | (= "dev")}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 
-  "coq-coqeal" {>= "1.0.3"}
-  "coq-mathcomp-real-closed" {>= "1.0.4"}
+  "coq-coqeal" {>= "1.0.5"}
+  "coq-mathcomp-real-closed" {>= "1.1.2"}
   "coq-mathcomp-bigenough" {>= "1.0.0"}
 ]
 

include/ops_header.v

@@ -1,5 +1,3 @@
-Require Import Psatz.
-Require Import Field.
 Require Import ZArith.
 
 From mathcomp Require Import all_ssreflect all_algebra.
@@ -15,7 +13,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GRing.Theory.
-Import Num.Theory.
+Import Order.TTheory GRing.Theory Num.Theory.
 
-Open Scope ring_scope.
+Local Open Scope ring_scope.

meta.yml

@@ -43,19 +43,45 @@ license:
   file: Licence_CeCILL-C_V1-en.txt
 
 supported_coq_versions:
-  text: 8.11
-  opam: '{>= "8.11" & < "8.12~"}'
+  text: 8.11 or later
+  opam: '{(>= "8.11" & < "8.15~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '1.10.0-coq-8.11'
+- version: '1.12.0-coq-8.11'
   repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.11'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
+- version: 'coq-8.11'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.12'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.13'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.14'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.10" & < "1.11~"}'
+    version: '{(>= "1.12" & < "1.14~") | (= "dev")}'
   description: |-
-    [MathComp ssreflect 1.10](https://math-comp.github.io)
+    [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
@@ -66,14 +92,14 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-coqeal
-    version: '{>= "1.0.3"}'
+    version: '{>= "1.0.5"}'
   description: |-
-    [CoqEAL 1.0.3 or later](https://github.com/CoqEAL/CoqEAL)
+    [CoqEAL 1.0.5 or later](https://github.com/CoqEAL/CoqEAL)
 - opam:
     name: coq-mathcomp-real-closed
-    version: '{>= "1.0.4"}'
+    version: '{>= "1.1.2"}'
   description: |-
-    [MathComp real closed fields 1.0.4 or later](https://github.com/math-comp/real-closed)
+    [MathComp real closed fields 1.1.2 or later](https://github.com/math-comp/real-closed)
 - opam:
     name: coq-mathcomp-bigenough
     version: '{>= "1.0.0"}'