Stream: Coq devs & plugin devs

Topic: CI broken (output test failure)

view this post on Zulip Gaëtan Gilbert (Jun 08 2023 at 15:22):

see https://github.com/coq/coq/pull/17707
the problem is https://github.com/coq/coq/pull/17628 getting merged without refreshing CI after https://github.com/coq/coq/pull/17117 which changed the output of the new test

view this post on Zulip Gaëtan Gilbert (Jun 08 2023 at 15:23):

I don't know why

Notation "'φ' x" := (id x) (at level 0) .

Check (φ 0).

prints φ (O) now but it does

view this post on Zulip Gaëtan Gilbert (Jun 09 2023 at 12:46):

could someone merge https://github.com/coq/coq/pull/17707 ?

view this post on Zulip Théo Zimmermann (Jun 09 2023 at 13:58):

Done

Last updated: Dec 05 2023 at 12:01 UTC