Stream: Coq devs & plugin devs

Topic: Small naming question: subst_mps


view this post on Zulip Hugo Herbelin (Dec 27 2021 at 10:48):

The name subst_mps is rather cryptic to me. While most functions applying name substitution on data foo are called subst_foo, why not to rename subst_mps into subst_constr? Not that it is a particularly discriminatory name, but at least it is an easier name to remember.
To be more discriminatory, an alternative, even if less consistent with other names, could be subst_modpaths_constr?
Or, conversely, to rename all subst_foo into subst_mps_foo, or subst_modpaths_foo?


Last updated: Feb 06 2023 at 00:03 UTC