generalize_eqs_vars fix incorrect selection of variables to generalize#22001
Merged
coqbot-app / GitLab CI job test-suite:base+async (pull request)
completed
May 5, 2026 in 0s
Test has failed on GitLab CI
This job is allowed to fail.
We show below the last 40 lines of the trace from GitLab (the complete trace is available here).
Details
+ typeclasses eauto with foo)
+ :>
+ cls))
+ in
+ exact (hint c)) on
+ bar
+Debug: 122063:proof:2:2:0 1: looking for cls without backtracking
+Debug: 122063:proof:2:2:0 1.1: exact c on cls, 0 subgoal(s)
Debug:
-1.1: (*external*) (let c :=
- constr:((ltac:(typeclasses eauto with foo) :> cls))
- in
- exact (hint c)) on
- bar, 0 subgoal(s)
+122063:proof:2:2:0 1.1: (*external*) (let c :=
+ constr:
+ ((ltac:(
+ typeclasses eauto with foo)
+ :>
+ cls))
+ in
+ exact (hint c)) on
+ bar, 0 subgoal(s)
0m0.000000s 0m0.000000s
0m0.230000s 0m0.130000s
==========> FAILURE <==========
output/TypeclassDebug.v ... Error! (unexpected output)
FAILURES
output/TypeclassDebug.v ... Error! (unexpected output)
make[1]: *** [Makefile:311: report] Error 1
make[1]: Leaving directory '/builds/coq/coq/test-suite'
make: *** [Makefile:231: all] Error 2
Uploading artifacts for failed job
Uploading artifacts...
test-suite/logs: found 4 matching artifact files and directories
Uploading artifacts as "archive" to coordinator... 201 Created correlation_id=01KQW33SK0ASH9CBBFVRNGZVYC id=7287488 responseStatus=201 Created token=64_h5dx45
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
Loading