Slight improvement in naming anonymous variables in error messages:

using closer naming strategies for naming variables in make_all_name_different
and when contracting trivial letins.

Not sure what the best policy is. Maybe the contraction process should
not invent names at al and let make_all_name_different do the job.

Maybe pretyping should name all rels which it pushes to environment
(with cases.ml paying attention to avoid clash).

The problem shows for instance with a PretypeError (... env, ... ,
ActualTypeNotCoercible (NotClean (... env ...)) message with two
copies of env which we don't if they are the same but which have to
share same names for similar rendering of the rels!

This was revealed e.g. by the error message of #4177.

0 files changed, 0 insertions, 0 deletions