Pick 8.20~2025.01:

- updated coq-mathcomp-real-closed to version 2.0.2 and enabled it
- updated coq-coqeal to version 2.0.3 and enabled it
- updated coq-mathcomp-analysis to version 1.8.0 (the above two updates depend on this)

package_picks/package-pick-8.20~2025.01.sh

@@ -87,7 +87,7 @@ then
   PACKAGES="${PACKAGES} coq-mathcomp-character.2.3.0"
   PACKAGES="${PACKAGES} coq-mathcomp-bigenough.1.0.1"
   PACKAGES="${PACKAGES} coq-mathcomp-finmap.2.1.0"
-# PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.1" # ToDo requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, fails with version restriction relaxation
+  PACKAGES="${PACKAGES} coq-mathcomp-real-closed.2.0.2"
   PACKAGES="${PACKAGES} coq-mathcomp-zify.1.5.0+2.0+8.16"
 # PACKAGES="${PACKAGES} coq-mathcomp-multinomials.2.2.0" # ToDo requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, fails with version restriction relaxation
   PACKAGES="${PACKAGES} coq-coquelicot.3.4.2"
@@ -140,12 +140,12 @@ then
     PACKAGES="${PACKAGES} z3_tptp.4.13.0" # ToDo Check
   fi
   PACKAGES="${PACKAGES} coq-paramcoq.1.1.3+coq8.20"
-  # PACKAGES="${PACKAGES} coq-coqeal.2.0.2" # ToDo: requires downgrade coq-mathcomp-ssreflect 2.3.0 to 2.2.0, depends on packages which fail with version relaxation
+  PACKAGES="${PACKAGES} coq-coqeal.2.0.3"
   PACKAGES="${PACKAGES} coq-libhyps.2.0.8"
   PACKAGES="${PACKAGES} coq-itauto.8.20.0"
 
   # General mathematics (which requires one of the above tools)
-  PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.7.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-analysis.1.8.0"
   PACKAGES="${PACKAGES} coq-mathcomp-algebra-tactics.1.2.3" # Works with version relaxation
   PACKAGES="${PACKAGES} coq-relation-algebra.1.7.11"