Make coqchk (make verify) work
Currently, make verify
fails with a stack overflow while checking iris.prelude.pretty.pretty_N_inj
. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/show_bug.cgi?id=4788). Can we find a similar work-around here?