Add new tactic "ensatz" for proving polynomial equalities with existential quantifier #554
Triggered via pull request
November 17, 2025 14:55
lyonel2017
lyonel2017
synchronize
#160
Status
Success
Total duration
1h 10m 26s
Artifacts
–
nix-action-rocq-9.0.yml
on: pull_request_target
rocq-core
1m 1s
stdlib-warnings
3m 57s
argosy
2m 0s
atbr
2m 16s
bbv
1m 37s
coinduction
1m 30s
coqutil
2m 12s
dpdgraph-test
1m 38s
flocq
2m 37s
kami
4m 31s
neural-net-coq-interp
2m 26s
paramcoq-test
1m 32s
rocq-lean-import
1m 52s
smtcoq
2m 11s
stdpp
2m 46s
tlc
1m 58s
waterproof
2m 15s
stdlib-refman-html
3m 59s
rocq-elpi-test
2m 17s
quickchick-test
1m 7s
metarocq-translations
1m 4s
http
2m 24s
fcsl-pcm
1m 10s
Verdi
1m 13s
mathcomp-word
2m 0s
deriving
1m 8s
mathcomp-algebra-tactics
1m 13s
mathcomp
1m 7s
mathcomp-analysis-stdlib
1m 6s