diff options
| author | Hugo Herbelin | 2015-09-16 08:42:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-16 08:48:05 +0200 |
| commit | e91327a01f725f6c709adba9ddf3b41212b488ca (patch) | |
| tree | fa90324319ccd7beb12c446f22fee8ec6be3dc3f /kernel/type_errors.ml | |
| parent | 95903cc3bcb9aed92459e644d295be4d9ca25405 (diff) | |
Continuing investigation on how to preserve the locality of the action
of "apply ... in ... as ..." in the context.
Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is
created, the statement of the refined hypothesis virtually depends on
the whole context and has to be left at the top.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions