Add new tactic "ensatz" for proving polynomial equalities with existential quantifier #549
Triggered via pull request
November 17, 2025 14:55
lyonel2017
lyonel2017
synchronize
#160
Status
Success
Total duration
1h 53m 32s
Artifacts
–
nix-action-rocq-master.yml
on: pull_request_target
rocq-core
1m 8s
argosy
1m 45s
atbr
2m 22s
bbv
1m 33s
coinduction
1m 29s
coq-performance-tests
15m 32s
coq-tools
7m 9s
cross-crypto
6m 17s
dpdgraph-test
1m 31s
engine-bench
5m 27s
fiat-parsers
5m 21s
itauto
2m 56s
neural-net-coq-interp
2m 1s
paramcoq-test
1m 41s
perennial
13m 58s
rocq-lean-import
1m 50s
smtcoq
2m 11s
tlc
2m 6s
waterproof
2m 27s
rocq-elpi-test
2m 8s
mtac2
2m 5s
equations-test
1m 8s
coq-hammer
1m 3s
stalmarck-tactic
1m 5s
fiat-crypto-legacy
1m 18s
corn
7m 41s
VST
16m 6s
relation-algebra
2m 48s
coquelicot
1m 10s
quickchick-test
1m 19s
iris-examples
1m 13s
http
3m 12s
category-theory
6m 52s
deriving
2m 20s
mathcomp-word
1m 20s
fcsl-pcm
3m 3s
fiat-crypto-ocaml
13m 32s
VerdiRaft
6m 15s
mathcomp-algebra-tactics
1m 13s
mathcomp
1m 48s
mathcomp-analysis-stdlib
2m 42s
metarocq-test
3m 13s