Frédéric Besson

Results 36 comments of Frédéric Besson

Tify + lra solves programs mixing Z and R

> CI is getting the overlay commit AFAICT https://gitlab.inria.fr/coq/coq/-/jobs/5517508#L1430 Good. And for some reason, the CI goes further than my previous attempt.

Tify + lra solves programs mixing Z and R

@coqbot run full ci

Tify + lra solves programs mixing Z and R

@coqbot run full ci

Tify + lra solves programs mixing Z and R

@coqbot run full ci

Tify + lra solves programs mixing Z and R

@coqbot run full ci

Tify + lra solves programs mixing Z and R

I am confused. It seems the CI turns deprecation messages into errors... That looks inconvenient...