Random observation while reading code: `UnivSubst.subst_univs_constr`

(via `subst_univs_fn_constr`

) does not nothing special for `Array`

but `Vars.subst_instance_constr`

does have a case for `Array`

. Could this be a bug?

To be clear(er): I had expected to find a case for `Array`

because it is the one(?) kind of term that directly carries universes apart from constants, constructors, inductives, and sorts.

probably buggy yes

we have too many versions of this function

It seems that `UnivSubst.subst_univs_constr`

is only used when registering hints on arbitrary constr (indirectly via `EConstr.Vars.subst_univs_constr`

)

https://github.com/coq/coq/pull/14247

Last updated: Sep 09 2024 at 06:02 UTC