Stream: Coq users

Topic: pow_pos_strict moved?


view this post on Zulip Ralf Jung (Jun 16 2021 at 18:41):

I am seeing a CI failure with Coq master

The reference ZifyInst.pow_pos_strict was not found in the current

The same code works fine in 8.13.2. I am trying to figure out what happened with that lemma, but can't find anything by grepping the changelog folder or searching in GH PRs...

view this post on Zulip Gaëtan Gilbert (Jun 16 2021 at 18:43):

looks like it was deleted https://github.com/coq/coq/commit/8193ca191cc435c108a4842ae38a11d74c7c20a5

view this post on Zulip Ralf Jung (Jun 16 2021 at 18:44):

from that diff maybe pow_nonneg works as a substitute

view this post on Zulip Ralf Jung (Jun 16 2021 at 18:44):

but the deletion should still be mentioned in the changelog, shouldnt it?

view this post on Zulip Ralf Jung (Jun 16 2021 at 18:45):

hm, no, pow_nonneg gives me a but I need a <

view this post on Zulip Ralf Jung (Jun 16 2021 at 18:45):

ah, pow_pos_nonneg works :)

view this post on Zulip Gaëtan Gilbert (Jun 16 2021 at 19:44):

Ralf Jung said:

but the deletion should still be mentioned in the changelog, shouldnt it?

I don't know
somehow random lemmas in ZifyInst should be internal details, but we don't have the tech to make that happen

view this post on Zulip Ralf Jung (Jun 16 2021 at 22:36):

Would be good to at least hide them from SearchAbout (if it had not shown up there, I would not have used it to begin with)

view this post on Zulip Ralf Jung (Jun 16 2021 at 22:39):

e.g. SearchAbout could skip Local Lemma


Last updated: Feb 06 2023 at 12:04 UTC