Version constraints on coq-mathcomp-algebra-tactics.1.2.4 are incorrect for Coq 8.20.0

[JasonGross]

In docker image mathcomp/mathcomp:2.3.0-coq-8.20

2025-11-03T21:31:38.4296460Z #=== ERROR while compiling coq-mathcomp-algebra-tactics.1.2.4 =================#
2025-11-03T21:31:38.4297723Z # context              2.3.0 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.14.2+options | https://coq.inria.fr/opam/released#2025-08-14 12:33
2025-11-03T21:31:38.4298795Z # path                 ~/.opam/4.14.2+flambda/.opam-switch/build/coq-mathcomp-algebra-tactics.1.2.4
2025-11-03T21:31:38.4299424Z # command              /usr/bin/make -j3
2025-11-03T21:31:38.4299802Z # exit-code            2
2025-11-03T21:31:38.4300260Z # env-file             ~/.opam/log/coq-mathcomp-algebra-tactics-14-802943.env
2025-11-03T21:31:38.4300966Z # output-file          ~/.opam/log/coq-mathcomp-algebra-tactics-14-802943.out
2025-11-03T21:31:38.4301487Z ### output ###
2025-11-03T21:31:38.4301759Z # [...]
2025-11-03T21:31:38.4302534Z # New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
2025-11-03T21:31:38.4303951Z # [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
2025-11-03T21:31:38.4304670Z # [ambiguous-paths,coercions,default]
2025-11-03T21:31:38.4305142Z # File "./theories/lra.v", line 396, characters 0-32:
2025-11-03T21:31:38.4305553Z # Error:
2025-11-03T21:31:38.4306304Z # File "/home/coq/.opam/4.14.2+flambda/.opam-switch/build/coq-mathcomp-algebra-tactics.1.2.4/theories/lra.elpi", line 782, characters 2-5
2025-11-03T21:31:38.4307377Z # ignoring flexible clause: Env [elpi.flex-clause,elpi.typecheck,elpi,default]
2025-11-03T21:31:38.4308090Z # 
2025-11-03T21:31:38.4308591Z # make[2]: *** [Makefile.coq:818: theories/lra.vo] Error 1
2025-11-03T21:31:38.4309155Z # make[2]: *** [theories/lra.vo] Deleting file 'theories/lra.glob'
2025-11-03T21:31:38.4309654Z # make[1]: *** [Makefile.coq:417: all] Error 2
2025-11-03T21:31:38.4310116Z # make: *** [Makefile:23: invoke-coqmakefile] Error 2
2025-11-03T21:31:38.4310423Z 
2025-11-03T21:31:38.7646535Z 
2025-11-03T21:31:38.7646576Z 
2025-11-03T21:31:38.7647167Z <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
2025-11-03T21:31:38.7647946Z +- The following actions failed
2025-11-03T21:31:38.7648480Z | - build coq-mathcomp-algebra-tactics 1.2.4
2025-11-03T21:31:38.7648982Z +- 
2025-11-03T21:31:38.7649342Z +- The following changes have been performed
2025-11-03T21:31:38.7649658Z | - install conf-g++               1.0
2025-11-03T21:31:38.7649932Z | - install coq-compcert           3.15
2025-11-03T21:31:38.7650228Z | - install coq-coquelicot         3.4.4
2025-11-03T21:31:38.7650504Z | - install coq-flocq              4.2.1
2025-11-03T21:31:38.7650795Z | - install coq-interval           4.11.3
2025-11-03T21:31:38.7651085Z | - install coq-mathcomp-analysis  1.12.0
2025-11-03T21:31:38.7651373Z | - install coq-mathcomp-bigenough 1.0.2
2025-11-03T21:31:38.7651674Z | - install coq-mathcomp-classical 1.12.0
2025-11-03T21:31:38.7651958Z | - install coq-mathcomp-finmap    2.2.1
2025-11-03T21:31:38.7652245Z | - install coq-mathcomp-reals     1.12.0
2025-11-03T21:31:38.7652553Z | - install coq-mathcomp-zify      1.5.0+2.0+8.16
2025-11-03T21:31:38.7652863Z | - install coq-menhirlib          20240715
2025-11-03T21:31:38.7653262Z | - install coq-record-update      0.3.4
2025-11-03T21:31:38.7653831Z | - install coq-vcfloat            2.3
2025-11-03T21:31:38.7654268Z | - install coq-vst                2.15
2025-11-03T21:31:38.7654639Z | - install coq-vst-lib            2.15.1
2025-11-03T21:31:38.7655102Z | - install coq-vst-zlist          2.13
2025-11-03T21:31:38.7655470Z | - install rocq-mathcomp-finmap   2.2.1
2025-11-03T21:31:38.7655902Z +- 
2025-11-03T21:31:38.7656310Z 

https://productionresultssa11.blob.core.windows.net/actions-results/a42ff28f-fef3-43e9-b59b-7564a27597d8/workflow-job-run-98652adb-16fe-58ae-bd83-e3b5c76aa7ca/logs/job/job-logs.txt?rsct=text%2Fplain&se=2025-11-03T22%3A32%3A26Z&sig=8DJtnYmTZ9I2s%2BIIAIqVDeDdHNPGy930AphLslk52oU%3D&ske=2025-11-04T08%3A14%3A18Z&skoid=ca7593d4-ee42-46cd-af88-8b886a2f84eb&sks=b&skt=2025-11-03T20%3A14%3A18Z&sktid=398a6654-997b-47e9-b12b-9515b896b4de&skv=2025-11-05&sp=r&spr=https&sr=b&st=2025-11-03T22%3A22%3A21Z&sv=2025-11-05