Putting back the subst_defined_metas_evars function in the old term API.

It seems this is a performance-critical function for unification-heavy code.
In particular, tactics relying on meta unification suffered an important
penalty after this function was rewritten with the evar-insensitive API, as
witnessed e.g. by Ncring_polynom whose compilation time increased by ~30%.

I am not sure about the specification of this function, but it seems safer
to revert the changes and just do it the old way. It may even disappear if
we get rid of the old unification algorithm at some point.

0 files changed, 0 insertions, 0 deletions