Random observation while reading code:
subst_univs_fn_constr) does not nothing special for
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
Last updated: Dec 06 2023 at 15:01 UTC