Gaëtan Gilbert (Sep 23 2020 at 13:56): Gaëtan Gilbert (Sep 23 2020 at 13:56):The notes for the 2020-09-09 call say some "--no-qed-check" flag was discussed but doesn't explain what it's supposed to do.
Is it different from vos mode?
Gaëtan Gilbert (Sep 23 2020 at 13:56):cc @Arthur Charguéraud
Last updated: Dec 07 2023 at 17:01 UTC