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?

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

Oh, thanks

from what I remember, the `zify`

stuff disappeared for me in `coqchk`

somewhere around 8.16

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

Last updated: Jun 13 2024 at 21:01 UTC