diff options
| author | Hugo Herbelin | 2018-08-04 11:55:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-24 18:10:55 +0200 |
| commit | 5780336e3be522f76906b719c3d3694f243a5bdb (patch) | |
| tree | 35bf477a6f216b2f75fecbc6caeb9fbadfa0f6f7 /kernel/cbytecodes.ml | |
| parent | fb8365e96ccb5d25d3810af99c36e7b27fec8fad (diff) | |
Fixes #8215 ("critical" bug of type inference in interpreting evars by names).
When interpreting an existential variable "?n@{inst}" in the current
context, check that variables bound to local definitions are replaced
by variables with convertible body.
Also give a message explaining the type error or non-convertibility
error rather than wrongly saying that there is no binding for the
variable.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions