diff options
| author | aspiwack | 2013-11-04 18:08:51 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-04 18:08:51 +0000 |
| commit | 6fea2f181221155535fdd86f67ae10077876ca6d (patch) | |
| tree | f65aa64d360ee5826a516f2cb1fe5b668968cc87 /pretyping | |
| parent | 84b30df7b5ef9479a89de322bceee5619405d195 (diff) | |
Nicer infered names in refine.
When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index c8481bca74..2b28c1a752 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -338,7 +338,7 @@ let push_rel_context_to_named_context env typ = let (subst, vsubst, _, env) = Context.fold_rel_context (fun (na,c,t) (subst, vsubst, avoid, env) -> - let id = next_name_away na avoid in + let id = next_ident_away (id_of_name_using_hdchar env t na) avoid in match extract_if_neq id na with | Some id0 when not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new |