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: Oct 15 2021 at 21:02 UTC