Stream: Coq devs & plugin devs

Topic: typeops and ==


view this post on Zulip Enrico Tassi (Oct 09 2020 at 09:26):

The code of execute goes a long way in using == in order to not re-allocate if the calls on sub-terms do not change the term. I could not find the piece of code that could do that. Which branch of execute does not return the input term?

view this post on Zulip Gaëtan Gilbert (Oct 09 2020 at 09:27):

when it needs to fix relevance

view this post on Zulip Gaëtan Gilbert (Oct 09 2020 at 09:28):

(check_assumption etc)

view this post on Zulip Enrico Tassi (Oct 09 2020 at 09:36):

was the code doing == there even before sProp?

view this post on Zulip Gaëtan Gilbert (Oct 09 2020 at 09:43):

the code only returned the type before sprop

view this post on Zulip Enrico Tassi (Oct 09 2020 at 10:32):

ok, thanks

view this post on Zulip Matthieu Sozeau (Oct 12 2020 at 12:03):

Well, it used to return the same term for a while, then I optimized it away, and Gaëtan went back to returning a modified term for SProp


Last updated: Oct 16 2021 at 09:07 UTC