Why are terms evar-normalized during pretyping in cases.ml
?
Sometimes just to check which variables are free you need to do that
In evarsolve.ml#L1738-1741
, is it normal that this evar definition can happen to "disallowed" variables ?
what is "disallowed"?
not is_evar_allowed
probably someone forgot to put the check in that code
Last updated: Oct 13 2024 at 01:02 UTC