Stream: Coq devs & plugin devs

Topic: UnivSubst and Array


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 04 2021 at 11:59):

probably buggy yes
we have too many versions of this function

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (May 04 2021 at 12:24):

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


Last updated: Oct 15 2021 at 21:02 UTC