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