Anyone know why reduce_to_ind_gen use the tacred reduction hnf_constr
? https://github.com/coq/coq/blob/4cb847934949e89a644a5dedb4306cd54d91096c/pretyping/tacred.ml#L1273
You mean: Instead of using whd_all
? That is a good question.
Not sure. Doesn't hnf_constr
better preserve the name of constants unfolding to a fix
?
Last updated: Oct 13 2024 at 01:02 UTC