Hugo Herbelin (Dec 27 2021 at 10:48): 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: Dec 07 2023 at 14:02 UTC