From e0d36d4afd7f38eb6816b92d03ecc2d2f7dc8d3f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 22:08:31 +0200
Subject: 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.
---
 pretyping/namegen.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 5aca11ae61..a88c2e20e3 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -278,6 +278,7 @@ let make_all_name_different env =
   let avoid = ref (ids_of_named_context (named_context env)) in
   process_rel_context
     (fun (na,c,t) newenv ->
+       let na = named_hd newenv t na in
        let id = next_name_away na !avoid in
        avoid := id::!avoid;
        push_rel (Name id,c,t) newenv)
-- 
cgit v1.2.3