diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-02-13 14:36:18 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-13 14:36:18 +0100 |
commit | dcb23edad4debc0f4856580910cb5eba00077006 (patch) | |
tree | 85718e43abd3b791bd6de478196b39531db7230b /pretyping/detyping.mli | |
parent | dc9b65741dae1b2bf58394e26c9155dad2bf7591 (diff) |
Better error message for nested module application.
Fixes #3809.
Diffstat (limited to 'pretyping/detyping.mli')
0 files changed, 0 insertions, 0 deletions