Frédéric Besson

Results 36 comments of Frédéric Besson

[tauto] change proof search strategy

@coqbot run full ci

[tauto] change proof search strategy

@coqbot run full ci

[tauto] change proof search strategy

@coqbot run full ci

[tauto] change proof search strategy

Whether it is worth merging is up to you. Advantage (in rare cases) + it solves a few more goals + exponential improvement (for pathological cases) Disadvantage + slower for...

[tauto] change proof search strategy

@coqbot run full ci

Tify + lra solves programs mixing Z and R

> Définitely not 9.0.0 material (now that we have the rc, only bugfixes and doc improvements should go there) I agree! I never know where we are in the release...

Tify + lra solves programs mixing Z and R

@coqbot: run CI

Tify + lra solves programs mixing Z and R

@coqbot: run full CI

Tify + lra solves programs mixing Z and R

> @fajb if you want to run the full CI nowadays you need to ask `@coqbot run full CI` (or put the `request: full CI` label before pushing) I have...

Tify + lra solves programs mixing Z and R

Hi @andres-erbsen, good to know this is an interesting feature. Actually, I need help to run the CI. Though, I think I added an overlay for the stdlib, it seems...