Janno (May 04 2021 at 11:56): Janno (May 04 2021 at 11:56):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?
Janno (May 04 2021 at 11:58):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.
Gaëtan Gilbert (May 04 2021 at 11:59):probably buggy yes
we have too many versions of this function
Janno (May 04 2021 at 12:04):It seems that UnivSubst.subst_univs_constr is only used when registering hints on arbitrary constr (indirectly via EConstr.Vars.subst_univs_constr)
Gaëtan Gilbert (May 04 2021 at 12:24):https://github.com/coq/coq/pull/14247
Last updated: Sep 09 2024 at 06:02 UTC