compatibility with mathcomp 1.10.0 (#166)

.travis.yml

@@ -19,8 +19,8 @@ env:
   - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.8"
   - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.9"
   - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10"
-
-
+  - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.9"
+  - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.10"
 
 install: |
   # Prepare the COQ container

opam

@@ -20,9 +20,8 @@ install: [
 ]
 depends: [
   "coq" { ((>= "8.8" & < "8.11~") | = "dev") }
-  "coq-mathcomp-field"       {(>= "1.8.0" & < "1.10~")}
-  "coq-mathcomp-bigenough"   {(>= "1.0.0" & < "1.1~")}
-  "coq-mathcomp-finmap"      {(>= "1.2.0" & < "1.4~")}
+  "coq-mathcomp-field"       {(>= "1.8.0" & <= "1.10.0")}
+  "coq-mathcomp-finmap"      {(>= "1.2.0" & <= "1.4.0")}
 ]
 synopsis: "An analysis library for mathematical components"
 description: """
@@ -31,3 +30,11 @@ the Coq proof-assistant and using the Mathematical Components library.
 
 It is inspired by the Coquelicot library.
 """
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword: analysis"
+  "keyword: topology"
+  "keyword: real numbers"
+  "logpath: mathcomp-analysis"
+  "date:2019-12-03"
+]

theories/altreals/discrete.v

@@ -130,17 +130,17 @@ End Countable.
 (* -------------------------------------------------------------------- *)
 Section CountableTheory.
 Lemma countable_countable (T : countType) (E : pred T) : countable E.
-Proof. by exists pickle unpickle; apply/pickleK. Qed.
+Proof. by exists choice.pickle choice.unpickle; apply/choice.pickleK. Qed.
 
 Section CanCountable.
 Variables (T : Type) (U : countType) (E : pred T).
 Variables (f : [psub E] -> U) (g : U -> [psub E]).
 
 Lemma can_countable : cancel f g -> countable E.
 Proof.
-pose p := pickle \o f; pose u n := omap g (unpickle n).
+pose p := choice.pickle \o f; pose u n := omap g (choice.unpickle n).
 move=> can_fg; apply (@Countable _ E p u) => x.
-by rewrite {}/u {}/p /= pickleK /= can_fg.
+by rewrite {}/u {}/p /= choice.pickleK /= can_fg.
 Qed.
 End CanCountable.
 

theories/topology.v

@@ -2156,16 +2156,13 @@ Lemma tychonoff (I : eqType) (T : I -> topologicalType)
     [set f : forall i, T i | forall i, A i (f i)].
 Proof.
 move=> Aco; rewrite compact_ultra => F FU FA.
-set subst_coord := fun i pi f j =>
-  match eqVneq i j with
-  | left e => eq_rect i T pi _ e
-  | _ => f j
-  end.
+set subst_coord := fun (i : I) (pi : T i) (f : forall x : I, T x) (j : I) =>
+  if eqP is ReflectT e then ecast i (T i) (esym e) pi else f j.
 have subst_coordT i pi f : subst_coord i pi f i = pi.
-  rewrite /subst_coord; case: (eqVneq i i) => [e|/negP] //.
+  rewrite /subst_coord; case: eqP => // e.
   by rewrite (eq_irrelevance e (erefl _)).
 have subst_coordN i pi f j : i != j -> subst_coord i pi f j = f j.
-  move=> inej; rewrite /subst_coord; case: (eqVneq i j) => [e|] //.
+  move=> inej; rewrite /subst_coord; case: eqP => // e.
   by move: inej; rewrite {1}e => /negP.
 have pr_surj i : @^~ i @` (@setT (forall i, T i)) = setT.
   rewrite predeqE => pi; split=> // _.