Stream: Coq users

Topic: `coqchk` output


view this post on Zulip Sergey Bozhko (Sep 01 2023 at 06:53):

Hi, I have Coq 8.13.2 and ssreflect 1.12.0, when I run coqchk in my project, I get a bunch of these:

* Axioms:
    <...>
    Coq.micromega.ZifyInst.ltac_gen_subproof20
    Coq.micromega.ZifyInst.ltac_gen_subproof19
    Coq.micromega.ZifyInst.ltac_gen_subproof18
    Coq.micromega.ZifyInst.ltac_gen_subproof17
    Coq.micromega.ZifyInst.ltac_gen_subproof16
    Coq.micromega.ZifyInst.ltac_gen_subproof15

What is that? Where can I read about it?

view this post on Zulip Janno (Sep 01 2023 at 07:01):

Hey Sergey! I think this is a bug (which is still open AFAICT): https://github.com/coq/coq/issues/13324

view this post on Zulip Sergey Bozhko (Sep 01 2023 at 07:08):

Oh, thanks

view this post on Zulip Karl Palmskog (Sep 01 2023 at 07:42):

from what I remember, the zify stuff disappeared for me in coqchk somewhere around 8.16

view this post on Zulip Sergey Bozhko (Sep 04 2023 at 08:07):

True. Unfortunately I'm kind of stuck with Coq 8.13 in one project


Last updated: Jun 13 2024 at 21:01 UTC