From b0db472f18839c55963dacedbdb8a6f80a28342a Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Thu, 5 Dec 2019 20:42:37 +0900
Subject: [PATCH] compatibility with mathcomp 1.10.0 (#166)

---
 .travis.yml                  |  4 ++--
 opam                         | 13 ++++++++++---
 theories/altreals/discrete.v |  6 +++---
 theories/topology.v          | 11 ++++-------
 4 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 0934e5a78..390927809 100644
--- a/.travis.yml
+++ b/.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
diff --git a/opam b/opam
index b978d7f8b..99eaed7cc 100644
--- a/opam
+++ b/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"
+]
diff --git a/theories/altreals/discrete.v b/theories/altreals/discrete.v
index 9e0da40b7..7af7ac5e4 100644
--- a/theories/altreals/discrete.v
+++ b/theories/altreals/discrete.v
@@ -130,7 +130,7 @@ 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).
@@ -138,9 +138,9 @@ 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.
 
diff --git a/theories/topology.v b/theories/topology.v
index 49e8b63eb..682c96279 100644
--- a/theories/topology.v
+++ b/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=> // _.