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 /kernel/type_errors.ml | |
| 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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions