Stream: Coq devs & plugin devs

Topic: Evar normalization during case pretyping


view this post on Zulip Yann Leray (Feb 20 2024 at 23:47):

Why are terms evar-normalized during pretyping in cases.ml ?

view this post on Zulip Matthieu Sozeau (Feb 21 2024 at 08:22):

Sometimes just to check which variables are free you need to do that

view this post on Zulip Yann Leray (Feb 21 2024 at 13:20):

In evarsolve.ml#L1738-1741, is it normal that this evar definition can happen to "disallowed" variables ?

view this post on Zulip Gaëtan Gilbert (Feb 21 2024 at 13:28):

what is "disallowed"?

view this post on Zulip Yann Leray (Feb 21 2024 at 13:29):

not is_evar_allowed

view this post on Zulip Gaëtan Gilbert (Feb 21 2024 at 13:35):

probably someone forgot to put the check in that code


Last updated: Oct 13 2024 at 01:02 UTC