diff options
| author | Hugo Herbelin | 2015-07-16 22:08:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-16 22:16:19 +0200 |
| commit | e0d36d4afd7f38eb6816b92d03ecc2d2f7dc8d3f (patch) | |
| tree | 90360a403a69bb2f80bcb66d73a9505082997354 | |
| parent | 0b3a335219e161dc04f6734e9ee4f7c08cde6cd5 (diff) | |
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.
| -rw-r--r-- | pretyping/namegen.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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) |