prepare for https://github.com/coq/coq/pull/16289
Status | Pipeline | Created by | Stages | |
---|---|---|---|---|
Passed 00:12:19
| Stage: build |
Download artifacts
No artifacts found |
Due to a bug, eauto neglected the cost of the extern hint lia (and applied it first). However, if lia is applied last, then some non-useful low-cost hints introduce evars beforehand, which breaks the proof. Changing eauto to auto at the specific position would avoid the evar issue.
Status | Pipeline | Created by | Stages | |
---|---|---|---|---|
Passed 00:12:19
| Stage: build |
Download artifacts
No artifacts found |