Migrating to math-comp 1.11.0 (#34)

(changes should be backward compatible with mathcomp 1.11+beta1)

.travis.yml

@@ -15,12 +15,18 @@ env:
   - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.9"
   - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.10"
   - DOCKERIMAGE="mathcomp/mathcomp:1.11.0-coq-8.11"
+  # - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7"
+  # - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8"
+  # - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.9"
+  # - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.10"
+  # - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.11"
+  # - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.12"
 
 install:
 - docker pull ${DOCKERIMAGE}
 - docker tag  ${DOCKERIMAGE} ci:current
 - docker run  --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
-- docker exec CI /bin/bash --login -c "opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev"
+- docker exec CI /bin/bash --login -c "opam update -y"
 - docker exec CI /bin/bash --login -c "opam pin add -n coq-mathcomp-${CONTRIB} ."
 - docker exec CI /bin/bash --login -c "opam install --deps-only coq-mathcomp-${CONTRIB}"
 

opam

@@ -14,8 +14,8 @@ install: [
   [make "install"]
 ]
 depends: [
-  "coq" {(>= "8.7" & < "8.12~")}
-  "coq-mathcomp-ssreflect" {>= "1.11.0" & < "1.12~"}
+  "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.11" & < "1.12~") | (= "dev")}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {>= "1.0.0" & < "1.1~"}
   "coq-mathcomp-finmap"    {>= "1.5" & < "1.6~"}

src/mpoly.v

@@ -620,7 +620,7 @@ Definition multinom_porderMixin :=
   LePOrderMixin ltmc_def lemc_refl lemc_anti lemc_trans.
 
 Canonical multinom_porderType :=
-  Eval hnf in POrderType total_display 'X_{1..n} multinom_porderMixin.
+  Eval hnf in POrderType tt 'X_{1..n} multinom_porderMixin.
 
 Lemma leEmnm m1 m2 : (m1 <= m2)%O = (mdeg m1 :: val m1 <= mdeg m2 :: val m2)%O.
 Proof. by []. Qed.
@@ -665,15 +665,15 @@ Lemma lt_mdeg_ltmc (m1 m2 : 'X_{1..n}) :
 Proof. by rewrite ltEmnm ltxi_cons leEnat; case: ltngtP. Qed.
 
 Lemma mdeg_max (m1 m2 : 'X_{1..n}) :
-  mdeg (max m1 m2) = maxn (mdeg m1) (mdeg m2).
+  mdeg (m1 `|` m2)%O = maxn (mdeg m1) (mdeg m2).
 Proof.
 case: (leP m1 m2) => [/dup[]|].
   by move=> /join_idPl<- /lemc_mdeg/maxn_idPr->.
 by move/ltW=> /dup[] /join_idPr<- /lemc_mdeg/maxn_idPl.
 Qed.
 
 Lemma mdeg_bigmax (r : seq 'X_{1..n}) :
-  mdeg (\max_(m <- r) m)%O = \max_(m <- r) mdeg m.
+  mdeg (\join_(m <- r) m)%O = \max_(m <- r) mdeg m.
 Proof.
 elim: r => [|m r ih]; first by rewrite !big_nil mdeg0.
 by rewrite !big_cons mdeg_max ih.
@@ -763,7 +763,7 @@ elim/(@ltxwf _ [porderType of nat]): t m=> //=; last first.
   by rewrite /tof ltEsub/= -ltEmnm.
 move=> Q {ih} ih x; elim: x {-2}x (leqnn x).
   move=> x; rewrite leqn0=> /eqP->; apply/ih.
-  by move=> y; rewrite ltEnat ltn0.
+  by move=> y; rewrite ltEnat/= ltn0.
 move=> k wih l le_l_Sk; apply/ih=> y; rewrite ltEnat => lt_yl.
 by apply/wih; have := leq_trans lt_yl le_l_Sk; rewrite ltnS.
 Qed.
@@ -2058,7 +2058,7 @@ Variable R : ringType.
 
 Implicit Types p q r : {mpoly R[n]}.
 
-Definition mlead p : 'X_{1..n} := (\max_(m <- msupp p) m)%O.
+Definition mlead p : 'X_{1..n} := (\join_(m <- msupp p) m)%O.
 
 Lemma mleadC (c : R) : mlead c%:MP = 0%MM.
 Proof.
@@ -2147,7 +2147,7 @@ Qed.
 
 Lemma mlead_sum_le {T} (r : seq T) P F :
   (mlead (\sum_(p <- r | P p) F p)
-    <= \max_(p <- r | P p) (mlead (F p)))%O.
+    <= \join_(p <- r | P p) (mlead (F p)))%O.
 Proof.
 elim/big_rec2: _ => /= [|x m p Px le]; first by rewrite mlead0.
 by apply/(le_trans (mleadD_le _ _))/leU2.
@@ -2157,7 +2157,7 @@ Lemma mlead_sum {T} (r : seq T) P F :
   uniq [seq mlead (F p) | p <- r & P p] ->
 
      mlead (\sum_(p <- r | P p) F p)
-  = (\max_(p <- r | P p) (mlead (F p)))%O.
+  = (\join_(p <- r | P p) (mlead (F p)))%O.
 Proof.
 elim: r=> [|p r ih]; first by rewrite !big_nil mlead0.
 rewrite !big_cons /=; case: (P p)=> //= /andP[Fp_ml uq_ml].
@@ -4062,7 +4062,7 @@ case: (boolP P)=> [/existsP[/= i /andP[lt_ih i_notin_h]]|hNP]; last first.
     by move/eq2/negbTE. by move/eq1.
 pose i0 : 'I_n := [arg min_(j < i | j \notin h) j].
 apply/ltW/ltmcP; first by rewrite !mdeg_mesym1 card_mesymlmnm.
-exists i0; rewrite {}/i0; case: fintype.arg_minP => //=.
+exists i0; rewrite {}/i0; case: arg_minnP => //=.
 + move=> i0 i0_notin_h i0_min j lt_j_i0; rewrite !mnmE in_set.
   rewrite (@ltn_trans i) // 1?(@leq_trans i0) // ?i0_min //.
   by case: (boolP (j \in h))=> // /i0_min; rewrite leqNgt lt_j_i0.