diff options
author | 2015-02-13 14:36:18 +0100 | |
---|---|---|
committer | 2015-02-13 14:36:18 +0100 | |
commit | dcb23edad4debc0f4856580910cb5eba00077006 (patch) | |
tree | 85718e43abd3b791bd6de478196b39531db7230b /pretyping/pretype_errors.ml | |
parent | dc9b65741dae1b2bf58394e26c9155dad2bf7591 (diff) |
Better error message for nested module application.
Fixes #3809.
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions