Merge pull request #37 from thery/mathcomp1_15

work with mathcomp 1.15

.github/workflows/docker-action.yml

@@ -17,12 +17,12 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

README.md

@@ -23,7 +23,7 @@ Mathematical Components library.
   - Cyril Cohen, Inria (initial)
   - Laurent Théry, Inria
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.13, Coq 8.14, Coq 8.15
+- Compatible Coq versions: Coq 8.14 to Coq 8.15
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

coq-robot.opam

@@ -19,14 +19,14 @@ Mathematical Components library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") }
-  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.15~") }
-  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.15~") }
-  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") }
-  "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") }
-  "coq-mathcomp-analysis" { (>= "0.3.13") & (< "0.4~")}
-  "coq-mathcomp-real-closed" { (>= "1.1.2") }
+  "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") }
+  "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") }
+  "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") }
+  "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") }
+  "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") }
+  "coq-mathcomp-analysis" { (>= "0.5.0" & < "0.6~") }
+  "coq-mathcomp-real-closed" { (>= "1.1.3") }
 ]
 
 tags: [

derive_matrix.v

@@ -2,8 +2,9 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
-From mathcomp.analysis Require Import boolp reals Rstruct classical_sets posnum.
+From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed.
 From mathcomp.analysis Require Import topology normedtype landau forms derive.
+From mathcomp.analysis Require Import functions.
 Require Import ssr_ext euclidean rigid skew.
 
 (******************************************************************************)

differential_kinematics.v

@@ -2,8 +2,9 @@
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat.
 From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
 From mathcomp Require Import realalg complex fingroup perm.
-From mathcomp.analysis Require Import boolp reals Rstruct classical_sets posnum.
+From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed.
 From mathcomp.analysis Require Import topology normedtype landau forms derive.
+From mathcomp Require Import functions.
 Require Import ssr_ext derive_matrix euclidean frame rot skew rigid.
 
 (******************************************************************************)

meta.yml

@@ -30,57 +30,57 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.13, Coq 8.14, Coq 8.15
-  opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }'
+  text: Coq 8.14 to Coq 8.15
+  opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- 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-8.14'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.13'
+- version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.13.0" & < "1.15~") }'
+    version: '{ (>= "1.13.0" & < "1.16~") }'
   description: |-
     [MathComp ssreflect](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-fingroup
-    version: '{ (>= "1.13.0" & < "1.15~") }'
+    version: '{ (>= "1.13.0" & < "1.16~") }'
   description: |-
     [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{ (>= "1.13.0" & < "1.15~") }'
+    version: '{ (>= "1.13.0" & < "1.16~") }'
   description: |-
     [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-solvable
-    version: '{ (>= "1.13.0" & < "1.15~") }'
+    version: '{ (>= "1.13.0" & < "1.16~") }'
   description: |-
     [MathComp solvable](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{ (>= "1.13.0" & < "1.15~") }'
+    version: '{ (>= "1.13.0" & < "1.16~") }'
   description: |-
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "0.3.13") & (< "0.4~")}'
+    version: '{ (>= "0.5.0" & < "0.6~") }'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
     name: coq-mathcomp-real-closed
-    version: '{ (>= "1.1.2") }'
+    version: '{ (>= "1.1.3") }'
   description: |-
     [MathComp real closed](https://github.com/math-comp/real-closed)
 

rot.v

@@ -779,7 +779,7 @@ move=> u1.
 by rewrite orthogonalE tr_emx3 tr_spin inv_emx3 // exp_spin u1 expr1n scaleN1r.
 Qed.
 
-Lemma rank_eskew a w : norm w = 1 -> \rank `e^(a, w) = 3.
+Lemma rank_eskew a w : norm w = 1 -> \rank `e^(a, w) = 3%N.
 Proof.
 move=> w1; by rewrite mxrank_unit // orthogonal_unit // eskew_is_O.
 Qed.
@@ -790,7 +790,7 @@ move=> w1.
 move/orthogonal_det/eqP : (eskew_is_O (a / 2%:R) w1).
 rewrite -(@eqr_expn2 _ 2) // expr1n sqr_normr expr2 -det_mulmx.
 rewrite mulmxE emx3M; last by rewrite spin3 w1 expr1n scaleN1r.
-by move/eqP; rewrite -posnum.splitr.
+by move/eqP; rewrite -mathcomp_extra.splitr.
 Qed.
 
 Lemma eskew_is_SO a w : norm w = 1 -> `e^(a, w) \is 'SO[T]_3.