Preservation of the name of evars/goals when applying pose/set/intro/clearbody.

For pose/set/clearbody, I think it is clear that we want to preserve
the name and this commit do it.

For revert, I first did not preserve the name, then considered in
2ba2ca96be88 that it was better to preserve it.

For intro, like for revert actually, I did not preserve the name,
based on the idea that the type was changing (*). For instance if we have
?f:nat->nat, do we really want to keep the name f in ?f:nat after an
intro.

For revert, I changed my mind based on the idea that if we had a
better control of the name if we keep the name that if the system
invents a new one based on the type. I think this is more reasonable
than (*), so this commit preserves the name for intro.

For generalize, it is still not done because of generalize being in
the old proof engine.

0 files changed, 0 insertions, 0 deletions